No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
62theorem tick_is_atomic_time_unit :
63 ∀ (n : ℕ), n > 0 → (n : ℝ) * fundamental_tick ≥ fundamental_tick := by
proof body
Term-mode proof.
64 intro n hn
65 have : (1 : ℝ) ≤ n := Nat.one_le_cast.mpr hn
66 have htick_pos : fundamental_tick > 0 := tick_pos
67 nlinarith
68
69/-! ## II. Phi-Irrationality Implies Exact Computation Limits -/
70
71/-- **THEOREM IC-002.4**: φ is irrational.
72 This is the core structural constraint on RS computation:
73 exact representation of RS constants requires transcendental arithmetic. -/
depends on (13)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Phi
in IndisputableMonolith.Cost.AczelProof
decl_use
-
Phi
in IndisputableMonolith.Cost.AczelTheorem
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
fundamental_tick
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
tick_pos
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use