theorem proved term proof

`D_forces_eight_tick`

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

formal statement (Lean)

  66theorem D_forces_eight_tick : 2 ^ 3 = eight_tick := by rfl

proof body

Term-mode proof.

  67
  68/-! ## Speed of Light -/
  69
  70/-- c = ℓ₀ / τ₀ (derived from units, not measured).
  71
  72In RS: c is the ratio of fundamental length to fundamental time.
  73The SI value 299,792,458 m/s comes from calibration.
  74-/

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
eight_tick in IndisputableMonolith.Foundation.DimensionForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
eight_tick in IndisputableMonolith.Gap45.PhysicalMotivation decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
calibration in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
eight_tick in IndisputableMonolith.RRF.Foundation.Constants decl_use
eight_tick in IndisputableMonolith.Thermodynamics.RecognitionThermodynamics decl_use