ladder_cascade_bound
plain-language theorem explainer
The inequality bounds the J-cost of a summed phi-ladder rung by twice the sum of the separate rung costs plus twice their product. Researchers modeling ground-state instability and ladder population from T0-T8 cite it to keep cascade costs finite. The proof is a term-mode reduction that rewrites the combined exponent via power composition then invokes Jcost submultiplicativity on positive bases.
Claim. For all integers $a,b$, $Jcost(φ^{a+b}) ≤ 2 Jcost(φ^a) + 2 Jcost(φ^b) + 2 Jcost(φ^a) Jcost(φ^b)$, where $φ$ is the golden ratio and $Jcost$ is the cost function satisfying the d'Alembert-derived submultiplicative inequality for positive arguments.
background
The StillnessGenerative module derives from T0-T8 that the unique zero-defect state x=1 is unstable and generative: T4 forces non-trivial content because uniform states carry zero recognition information, while T7 requires an 8-tick period that a degenerate cycle violates. T6 then forces all non-trivial ratios to equal φ, with the Fibonacci relation φ^n + φ^{n+1} = φ^{n+2} populating the full ladder and ledger symmetry J(x)=J(1/x) reflecting positive and negative rungs. The local phi-ladder is the map n ↦ φ^n for n ∈ ℤ.
proof idea
The term proof unfolds the phi-ladder definition to expose a product of powers, rewrites the exponent sum via the phi_power_compose theorem, and applies the Jcost_submult lemma directly to the two positive powers supplied by phi_pos.
why it matters
The bound is used inside origin_question_resolved to close the finite-cost cascade argument that populates the entire ladder from the ground state. It supplies the concrete inequality needed for the Fibonacci step in the module's derivation chain, confirming that adjacent rungs compose without cost explosion while respecting T5 uniqueness of the zero-defect state and T6 closure on geometric sequences. The result therefore anchors the claim that creation remains inside the eight-tick octave with bounded J(φ) < 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.