theorem proved term proof

`alpha_locked_in_unit`

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

formal statement (Lean)

 141theorem alpha_locked_in_unit : 0 < alpha_locked ∧ alpha_locked < 1 :=

proof body

Term-mode proof.

 142  ⟨alpha_locked_pos, alpha_locked_lt_one⟩
 143
 144/-! ## §5. Demanded Recognition Rate -/
 145
 146/-- The recognition event rate demanded by Newtonian gravitational dynamics
 147    of mass M at dynamical time T_dyn.
 148
 149    Each Planck-mass element requires one ledger update per dynamical time:
 150        R_demand = M / (m_P · T_dyn)
 151
 152    In RS-native units with m_P = 1:
 153        R_demand = M / T_dyn -/

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
alpha_locked in IndisputableMonolith.Constants.ILG decl_use
alpha_locked_lt_one in IndisputableMonolith.Constants.ILG decl_use
alpha_locked_pos in IndisputableMonolith.Constants.ILG decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
alpha_locked in IndisputableMonolith.Gravity.SPARCFalsifier decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
alpha_locked in IndisputableMonolith.Physics.CouplingLockIn decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use