Exercise arbitrary function replay with sine oddness

[kim-em]

Summary

• recognize sin (-x) structurally through opaque operation keys
• instantiate sin x and -(sin x) using snapshot-local stable-key operation resolution
• prove every exact two-node append is a conservative extension of an arbitrary caller-program prefix
• replay sine, negation, instance, and Real.sin_neg certificates, then transport [-1,0] to the original expression
• derive the concrete theorem 0 ≤ x → x ≤ 2 → -1 ≤ Real.sin (-x) ∧ Real.sin (-x) ≤ 0
• test reordered operation tables, unrelated prior nodes, bad signatures, wrong appended recipes, wrong products, wrong schemas, and wrong proof methods

This is the first non-polynomial vertical through the arbitrary package framework. It does not depend on the rational endpoint experiment and does not use native_decide.

Verification

• lake build HexIntervalExperiment HexInterval.PropagatorE2EConformance HexInterval.SemanticReplayConformance HexInterval.PolicySessionConformance HexInterval.SinOddConformance
• python3 scripts/check_file_line_counts.py
• git diff --check

Review focus

• arbitrary-prefix soundness of appendExtends
• correspondence between runtime stable-key resolution and semantic operation witnesses
• non-vacuity of the concrete caller model and final real theorem
• whether the exact fresh-node recipe should stay separate from later CSE-aware certificate variants