IndisputableMonolith.Foundation.MaximalForcing.RSCostUniverse

   1import IndisputableMonolith.Foundation.MaximalForcing.RealityClosure
   2import IndisputableMonolith.Cost.AczelProof
   3import IndisputableMonolith.CostUniqueness
   4
   5/-!
   6# Maximal Forcing: the cost-layer realization (Phase 1 + Phase 2.1)
   7
   8This is the first concrete instantiation of the maximal-forcing scaffold. It
   9roots the program in an existing, published, sorry-free uniqueness theorem
  10rather than a fresh assumption.
  11
  12* The realization carrier is a candidate recognition cost `F : ℝ → ℝ`.
  13* Admissibility is the conjunction of the five gate conditions that the Law of
  14  Logic imposes on any cost (reciprocal symmetry, normalization, the Recognition
  15  Composition Law, calibration, continuity). The `AczelSmoothnessPackage`
  16  instance is supplied by `Cost.AczelProof`, so it is a proved instance, not an
  17  added hypothesis.
  18* The claim placed under closure is "F equals the canonical cost J on the
  19  positive reals."
  20
  21Phase 2.1 then discharges `Forced Lcost isJClaim` by wrapping
  22`law_of_logic_forces_jcost`. This proves the forced-register pattern end to end:
  23a real theorem of RS becomes a `ForcedInvariant` over an admissible class.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Foundation
  28namespace MaximalForcing
  29
  30open IndisputableMonolith.Cost.FunctionalEquation
  31
  32/-- Admissibility for the cost-function layer: a candidate cost `F : ℝ → ℝ`
  33satisfies the five gate conditions that the Law of Logic imposes on any
  34recognition cost. -/
  35def CostAdmissible (F : ℝ → ℝ) : Prop :=
  36  IsReciprocalCost F ∧ IsNormalized F ∧ SatisfiesCompositionLaw F ∧
  37    IsCalibrated F ∧ ContinuousOn F (Set.Ioi 0)
  38
  39/-- Loosest cost class `L0`: continuous candidate costs on the positive reals. -/
  40def L0 : AdmissibilityClass (ℝ → ℝ) where
  41  admissible := { F | ContinuousOn F (Set.Ioi 0) }
  42  label := "continuous candidate costs on (0,∞)"
  43
  44/-- Gate-tightened cost class `Lcost`: candidates satisfying all five gate
  45conditions. -/
  46def Lcost : AdmissibilityClass (ℝ → ℝ) where
  47  admissible := { F | CostAdmissible F }
  48  label := "cost-gate conditions (reciprocal, normalized, RCL, calibrated, continuous)"
  49
  50/-- `Lcost` is a tightening of `L0`: every gate-admissible cost is in particular
  51a continuous candidate cost. The strictness witness is deferred. -/
  52def tighten_L0_Lcost : Tightening L0 Lcost where
  53  subset := by
  54    intro F hF
  55    exact hF.2.2.2.2
  56  strict_witness := True
  57
  58/-- The forced claim of the cost layer: `F` equals the canonical cost `J` on the
  59positive reals. -/
  60def isJClaim : RealityClaim (ℝ → ℝ) where
  61  label := "F = Jcost on (0,∞)"
  62  holds := fun F => ∀ x : ℝ, 0 < x → F x = Cost.Jcost x
  63
  64/-- The cost-layer claim universe: realizations are candidate cost functions,
  65admissibility is the gate class, and the claim under closure is `isJClaim`. -/
  66def costUniverse : ClaimUniverse where
  67  Realization := ℝ → ℝ
  68  admissibility := Lcost
  69  claims := { isJClaim }
  70
  71/-- **Phase 2.1.** Over the gate class, "equals `J`" is forced. This wraps the
  72published uniqueness theorem `law_of_logic_forces_jcost` with no new content and
  73no new axioms: the `AczelSmoothnessPackage` instance comes from `Cost.AczelProof`.
  74-/
  75theorem forced_isJ : Forced Lcost.admissible isJClaim := by
  76  intro F hF x hx
  77  obtain ⟨hRecip, hNorm, hComp, hCalib, hCont⟩ := hF
  78  exact law_of_logic_forces_jcost F hRecip hNorm hComp hCalib hCont x hx
  79
  80/-- The claim `isJClaim` is in the closure of the cost universe. -/
  81theorem isJClaim_in_closure :
  82    InClosure Primitive.lawOfLogic costUniverse isJClaim := by
  83  show isJClaim ∈ costUniverse.claims
  84  exact Set.mem_singleton _
  85
  86/-- **Forced-register entry.** `isJClaim`, rooted at the Law-of-Logic primitive,
  87with a real proof of forcedness. This is the first populated slot of the Phase 2
  88forced register. -/
  89def isJForcedInvariant : ForcedInvariant Primitive.lawOfLogic costUniverse where
  90  claim := isJClaim
  91  in_closure := isJClaim_in_closure
  92  forced := forced_isJ
  93
  94/-- The cost-layer universe is fully classified: its single claim is forced,
  95hence the (transitional) classifier is total over its closure. -/
  96theorem costUniverse_classifier :
  97    ∀ C : RealityClaim costUniverse.Realization,
  98      InClosure Primitive.lawOfLogic costUniverse C → ClaimClassification costUniverse C := by
  99  intro C hC
 100  have hCeq : C = isJClaim := by
 101    have : C ∈ costUniverse.claims := hC
 102    exact Set.mem_singleton_iff.mp this
 103  subst hCeq
 104  exact ClaimClassification.forced forced_isJ
 105
 106/-- A real `MaximalClosureCert` for the cost-layer universe: every claim in its
 107closure is classified. This discharges `maximal_forcing_closure` unconditionally
 108for `costUniverse`. -/
 109def costUniverseCert : MaximalClosureCert Primitive.lawOfLogic costUniverse where
 110  classifies := costUniverse_classifier
 111
 112/-! ## Phase 3 / Phase 5: the gate tightening does real work
 113
 114The risk flagged in the execution plan is cheap tightening: if `Lcost` did not
 115actually change any classification, the forcing result would be cosmetic. The
 116following shows the `L0 → Lcost` tightening is effective for `isJClaim`. Over the
 117loose class `L0` (continuous candidate costs), "equals J" is *independent*: the
 118canonical cost `J` satisfies it, but the constant-zero cost (also continuous)
 119does not. The gate conditions are what force `J`, not relabeling. -/
 120
 121/-- Over the loose class `L0`, "equals J" is independent: `Jcost` is a continuous
 122candidate cost that satisfies it, and the constant-zero function is a continuous
 123candidate cost that does not. -/
 124theorem isJ_independent_over_L0 : Independent L0.admissible isJClaim := by
 125  refine ⟨Cost.Jcost, (fun _ => (0 : ℝ)), ?_, ?_, ?_, ?_⟩
 126  · show ContinuousOn Cost.Jcost (Set.Ioi 0)
 127    exact IndisputableMonolith.CostUniqueness.Jcost_continuous_pos
 128  · show ContinuousOn (fun _ => (0 : ℝ)) (Set.Ioi 0)
 129    exact continuousOn_const
 130  · intro x _; rfl
 131  · intro h
 132    have h2 := h 2 (by norm_num)
 133    simp only [Cost.Jcost] at h2
 134    norm_num at h2
 135
 136/-- **The tightening is legitimate, not cheap.** `isJClaim` is independent over
 137`L0` but forced over `Lcost`. The gate conditions do real classificatory work:
 138they convert a free claim into a forced one. This is the per-step legitimacy
 139evidence the Phase 5 ladder requires for the `L0 → Lcost` rung. -/
 140theorem tightening_L0_Lcost_effective :
 141    Independent L0.admissible isJClaim ∧ Forced Lcost.admissible isJClaim :=
 142  ⟨isJ_independent_over_L0, forced_isJ⟩
 143
 144end MaximalForcing
 145end Foundation
 146end IndisputableMonolith
 147