theorem proved tactic proof

`native_very_not_codata`

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

formal statement (Lean)

 198theorem native_very_not_codata : alphaG_codata < row_alphaG_pred := by

proof body

Tactic-mode proof.

 199  have h1 := alphaG_pred_lower
 200  have h0 : alphaG_codata < (1e9 : ℝ) := by
 201    unfold alphaG_codata; norm_num
 202  linarith [h0, h1]
 203
 204/-!
 205## Falsifier (one line)
 206
 207A CODATA-consistent dimensionless `α_G` in SI and the RS-native
 208`G m_e^2 / (ℏ c)` written with `electron_structural_mass` cannot be the same
 209real number: matching experiment requires the explicit SI mass bridge, not
 210identification of the raw coherence-mass value with the kilogram number.
 211-/
 212

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

cert in IndisputableMonolith.Masses.AlphaGScoreCard decl_use

depends on (26)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
consistent in IndisputableMonolith.Complexity.SAT.Backprop decl_use
G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
m_e in IndisputableMonolith.Constants.ProtonElectronMassRatio decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
alphaG_codata in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
alphaG_pred_lower in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
row_alphaG_pred in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
electron_structural_mass in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
electron_structural_mass in IndisputableMonolith.RRF.Physics.ElectronMass.Defs decl_use