lemma proved term proof

`kappaA_ne_zero`

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

formal statement (Lean)

 105lemma kappaA_ne_zero : kappaA ≠ 0 := by

proof body

Term-mode proof.

 106  simpa [kappaA] using Constants.phi_ne_zero
 107
 108/-! Ledger units (δ subgroup) -/
 109namespace LedgerUnits
 110
 111/-- The subgroup of ℤ generated by δ. We specialize to δ = 1 for a clean order isomorphism. -/

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
phi_ne_zero in IndisputableMonolith.Constants decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
phi_ne_zero in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
phi_ne_zero in IndisputableMonolith.PhiSupport.Lemmas decl_use
kappaA in IndisputableMonolith.RecogSpec.Scales decl_use