def definition def or abbrev

`strict_arith_universal_initial`

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

formal statement (Lean)

  18def strict_arith_universal_initial (R : StrictLogicRealization) :
  19    (StrictLogicRealization.arith R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=

proof body

Definition body.

  20  (StrictLogicRealization.toLightweight R).orbitEquivLogicNat
  21
  22/-- **Strict Universal Forcing.**
  23
  24For any two strict Law-of-Logic realizations, the arithmetic derived from
  25their native law data is canonically equivalent. -/

depends on (17)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization 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
arith in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
StrictLogicRealization in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
toLightweight in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use