ledgerConservation_eq_one
plain-language theorem explainer
The equality establishes that the ledger conservation ratio, defined as the sum of the reciprocal of phi and its square, equals one. Economists working within Recognition Science scaling would cite this to anchor double-entry bookkeeping in the phi-ladder framework. The proof is a short algebraic reduction that unfolds the definition, invokes the quadratic identity for phi, and applies field simplification followed by linear arithmetic.
Claim. $1/phi + 1/phi^2 = 1$
background
In the LedgerEconomics module the ledgerConservationRatio is the noncomputable definition 1/phi + 1/phi^2. This expression is forced by the golden-ratio relation phi^2 = phi + 1 that appears throughout the Recognition Science forcing chain. The eight-tick octave supplies the periodic structure that later maps onto economic phases.
proof idea
The term proof unfolds ledgerConservationRatio, introduces phi_ne_zero to clear the denominator, and substitutes the identity from phi_sq_eq. Field_simp reduces the resulting rational expression and linarith closes the arithmetic equality.
why it matters
The result supplies the conservation law that forces double-entry structure in phi-scaled ledgers. It sits inside the eight-tick octave construction (T7) and supports the economic-phases definitions that follow in the same module. The accompanying comment records the falsifiable bound phi^8 in (46,48) for octave growth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.