theorem proved term proof

`J_bit_bounds`

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

formal statement (Lean)

 102theorem J_bit_bounds : 0.11 < J_bit_val ∧ J_bit_val < 0.12 := by

proof body

Term-mode proof.

 103  rw [J_bit_eq_phi_minus]
 104  constructor
 105  · have h := phi_gt_onePointSixOne
 106    linarith
 107  · have h := phi_lt_onePointSixTwo
 108    linarith
 109
 110/-! ## Part 2: Curvature Cost from Q₃ Geometry -/
 111
 112/-- The number of faces of the D-hypercube (D-cube). F = 2D. -/

used by (1)

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

planck_scale_matching_cert in IndisputableMonolith.Constants.PlanckScaleMatching decl_use

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
phi_gt_onePointSixOne in IndisputableMonolith.Constants decl_use
phi_lt_onePointSixTwo in IndisputableMonolith.Constants decl_use
J_bit_eq_phi_minus in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
J_bit_val in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use