phi_blend_5_hop_weak
plain-language theorem explainer
The inequality (1/φ²)^5 < 0.01 shows that five-hop causal chains under blend rate η = 1/φ² stay detectable above the 0.01 threshold. Researchers bounding multi-hop reach in SpMV causal graphs cite this result when checking sufficiency of the 8-tick octave. The tactic proof chains a lower bound on φ through successive nlinarith estimates and closes with a direct norm_num comparison of the fifth power.
Claim. Let φ denote the golden ratio. Then $((1/φ^2)^5 < 0.01)$.
background
The Causal Propagation Ordering module examines whether SpMV propagation preserves directed causal order and whether the 8-tick octave permits detectable multi-hop chains. Blend rate η is fixed at 1/φ² ≈ 0.382; activation after k hops decays as η^k. The module documentation states that η^5 ≈ 0.008 lies below the practical threshold ε = 0.01, implying five-hop chains remain detectable but weak and that practical reach is approximately 4.8 hops.
proof idea
The proof invokes phi_gt_onePointFive to obtain φ > 1.618. It applies nlinarith to derive φ² > 2.618 and 1/φ² < 0.382. A norm_num step verifies 0.382^5 < 0.01. The final calc uses pow_lt_pow_left to chain the strict inequality (1/φ²)^5 < 0.382^5 < 0.01.
why it matters
This bound supports the module's effective_reach_bound and octave_sufficient_for_chain claims by confirming that η^5 remains above the 0.01 detection floor. It directly informs the T7 eight-tick octave landmark, showing that eight ticks suffice for chains up to roughly five hops under the Recognition Science blend rate. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.