dalembert_cascade
plain-language theorem explainer
The d'Alembert cascade theorem shows that the J-cost satisfies the d'Alembert relation on products and quotients of integer powers of the golden ratio phi. Researchers deriving cost propagation along the phi-ladder in the Recognition Science T0-T8 chain would cite it. The proof is a one-line wrapper that applies the general d'Alembert identity after supplying positivity of the powers.
Claim. For integers $a,b$, let $J$ be the J-cost and let $φ$ be the golden ratio. Then $J(φ^a · φ^b) + J(φ^a / φ^b) = 2J(φ^a) + 2J(φ^b) + 2J(φ^a)J(φ^b)$.
background
The StillnessGenerative module derives from T0-T8 that the ground state $x=1$ is unstable and generates all structure via the phi-ladder. The J-cost vanishes at 1 and obeys the functional relation $J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y)$ for positive reals. Upstream dalembert_identity states exactly this identity: 'The d'Alembert identity: J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y)'. PhiForcing supplies the golden ratio $φ$ together with its positivity.
proof idea
This is a one-line wrapper that invokes dalembert_identity after supplying the positivity witnesses zpow_pos PhiForcing.phi_pos a and zpow_pos PhiForcing.phi_pos b.
why it matters
The declaration fills the d'Alembert Cascade section of the module, enabling cost calculations to propagate across the phi-ladder forced by T6. It supports the claim that non-trivial content on a closed scale sequence forces ratio $φ$ and populates the ladder via Fibonacci relations. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.