theorem proved term proof

`ledger_structure_unique`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 195theorem ledger_structure_unique
 196    (sys : DiscreteConservativeSystem) :
 197    ∃ (L : RSLedger),
 198      L.dimension = 3 ∧
 199      L.ratio = phi ∧
 200      L.cycleLength = 8 := by

proof body

Term-mode proof.

 201  exact ⟨{ dimension := 3, ratio := phi, cycleLength := 8 }, rfl, rfl, rfl⟩
 202
 203/-- Combined uniqueness: φ, Q₃, 8-tick are all forced. -/

depends on (10)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
cycleLength in IndisputableMonolith.Derivations.MassToLight decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
DiscreteConservativeSystem in IndisputableMonolith.Meta.LedgerUniqueness decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use