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)
109theorem ledger_self_grounding : ledger_is_self_grounded := by
proof body
Term-mode proof.
110 intro x hx
111 exact Cost.Jcost_nonneg hx
112
113/-- **THEOREM IC-004.6**: The J-cost framework determines what "exists":
114 x exists (RSExists) iff J(x) = 0 iff x = 1. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
ic004_certificate
in IndisputableMonolith.Information.SimulationHypothesisStructure
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
Jcost_nonneg
in IndisputableMonolith.Cost
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Cost.JcostCore
decl_use
-
RSExists
in IndisputableMonolith.Foundation.CostFirstExistence
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
RSExists
in IndisputableMonolith.Foundation.OntologyPredicates
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Gravity.CoherenceCollapse
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Gravity.EnergyProcessingBridge
decl_use
-
ledger_is_self_grounded
in IndisputableMonolith.Information.SimulationHypothesisStructure
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Jcost_nonneg
in IndisputableMonolith.NavierStokes.PhiLadderCutoff
decl_use