octave_sufficient_for_4_hop
plain-language theorem explainer
The inequality (1/φ²)^4 > 0.02 shows that the blend rate η = 1/φ² yields activation above the 0.02 threshold after four hops in an 8-tick cycle. Researchers modeling SpMV propagation on directed causal graphs would cite it to confirm the octave length suffices for short chains. The proof obtains φ bounds from phi_gt_onePointFive and phi_lt_onePointSixTwo, tightens η via nlinarith, and chains the fourth-power comparison with norm_num.
Claim. Let η = 1/φ² where φ is the golden ratio. Then η⁴ > 0.02.
background
The module examines whether SpMV propagation on directed chains preserves causal ordering and whether the 8-tick octave suffices for multi-hop reach. The blend rate η is set to 1/φ², matching ETA_BLEND in the engine implementation. Upstream lemmas phi_gt_onePointFive and phi_lt_onePointSixTwo supply the concrete bounds 1.618 < φ < 1.62 used to control η from above and below. The module documentation states that this bound implies practical reach of approximately 4.8 hops for ε = 0.01.
proof idea
The tactic proof first applies phi_gt_onePointFive to obtain φ > 1.618, then nlinarith to bound φ² strictly between 2.618 and 2.62. It derives the reciprocal lower bound 1/φ² > 1/2.62, verifies (1/2.62)^4 > 0.02 by norm_num, and finishes with a calc block that applies pow_lt_pow_left to chain the strict inequalities.
why it matters
This theorem directly answers diagnostic question 2 in the module: the 8-tick octave (T7) is long enough for detectable 4-hop causal chains when bonds remain unidirectional. It supports the parent claim octave_sufficient_for_chain and the reach formula log(ε)/log(η) ≈ 4.8 hops. The result closes the loop on the forcing-chain requirement that D = 3 spatial dimensions and the eight-tick period together permit ordered propagation before shortcuts flatten the ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.