IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioSubstrateBlocker

   1import IndisputableMonolith.Gravity.SevenGaps.StationarityBridgeClosure
   2
   3/-!
   4# P2.1 terminal: the bare ledger lacks a deficit-source constitutive coupling
   5
   6## Headline
   7
   8`recognition_ratio_derived` does not follow from a bare
   9`RecognitionLedger`.  The missing premise is a **signed deficit-source
  10constitutive coupling**: a source strength `c_sigma = kappa_sigma *
  11delta_sigma`, coupled linearly to the total strain in the J-cost action.
  12
  13This is an exact blocker package, not a status flag:
  14
  15* coboundary strains telescope to zero around every closed cycle;
  16* imposing the desired total-strain budget already assumes the ratio
  17  conclusion, so the constrained-budget route is circular;
  18* one and the same bare two-cell J-ledger is induced by opposite signed
  19  source orientations, so no selector from bare ledgers can recover the
  20  signed source universally;
  21* after the named constitutive coupling is supplied, J-stationarity derives
  22  the recognition-ratio bridge and its cubic remainder;
  23* the sourced construction has a nontrivial, uniformly admissible
  24  small-mesh family.
  25
  26The missing premise below does not mention `xRatio`, `Real.log`, or the
  27desired ratio relation.  It supplies only the source data and its linear
  28coupling to the already proved J-cost action.  Thus the positive result does
  29not define the desired bridge as an assumption.
  30
  31Status: every declaration is THEOREM or definitional MODEL as identified
  32below.  There is no `sorry`, `admit`, new axiom, `native_decide`, boolean
  33status record, or `FullTheoryLedger` flag change.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace Gravity
  38namespace SevenGaps
  39
  40/-! ## 1. The exact missing premise -/
  41
  42/-- **MODEL (the exact premise missing from the bare ledger).**
  43
  44A signed deficit-source constitutive coupling supplies a channel count, the
  45hinge coupling and signed geometric deficit, and a source strength satisfying
  46
  47`sourceStrength sigma = kappa sigma * geometricDeficit sigma`.
  48
  49It also supplies the positive mesh scale and the structural small-source
  50bound needed by the cubic estimate.  No field mentions the recognition
  51ratio or its logarithm. -/
  52structure DeficitSourceConstitutiveCoupling (H : Type*) where
  53  channels : ℕ
  54  channels_pos : 1 ≤ channels
  55  kappa : H → ℝ
  56  geometricDeficit : H → ℝ
  57  sourceStrength : H → ℝ
  58  source_eq : ∀ σ, sourceStrength σ = kappa σ * geometricDeficit σ
  59  meshScale : ℝ
  60  meshScale_pos : 0 < meshScale
  61  source_dominated :
  62    ∀ σ, |sourceStrength σ| ≤ (channels : ℝ) * meshScale
  63
  64/-- The constitutive action named by the missing premise: summed J-cost
  65minus the signed source coupled linearly to total strain. -/
  66noncomputable def deficitSourceAction {H : Type*}
  67    (C : DeficitSourceConstitutiveCoupling H) (σ : H)
  68    (t : Fin C.channels → ℝ) : ℝ :=
  69  sourcedAction C.channels (C.sourceStrength σ) t
  70
  71/-- **THEOREM (kernel identification of the premise).** The constitutive
  72action is exactly the summed J-cost of the exponential strains minus the
  73linear deficit-source term.  This identifies the missing premise inside the
  74kernel without assuming any ratio relation. -/
  75theorem deficitSourceAction_eq_jcost_sum {H : Type*}
  76    (C : DeficitSourceConstitutiveCoupling H) (σ : H)
  77    (t : Fin C.channels → ℝ) :
  78    deficitSourceAction C σ t
  79      = (∑ i, Cost.Jcost (Real.exp (t i)))
  80          - C.sourceStrength σ / C.channels * ∑ i, t i :=
  81  sourcedAction_eq_jcost_sum C.channels (C.sourceStrength σ) t
  82
  83/-! ## 2. Supplying the premise closes the conditional derivation -/
  84
  85/-- The bridge derived from the named constitutive coupling by the unique
  86global minimizer of `deficitSourceAction`.  Its ratio relation is proved by
  87`stationaryRatio_cubic`; it is not a field of the premise. -/
  88noncomputable def ratioBridgeFromDeficitSourceCoupling {H : Type*}
  89    (C : DeficitSourceConstitutiveCoupling H) :
  90    RecognitionRatioBridge H :=
  91  recognitionRatioBridge_ofStationarity C.channels C.channels_pos
  92    C.kappa C.geometricDeficit C.meshScale C.meshScale_pos
  93    (fun σ => by
  94      rw [← C.source_eq σ]
  95      exact C.source_dominated σ)
  96
  97/-- **THEOREM (the conditional `recognition_ratio_derived`).** Once the
  98named deficit-source constitutive coupling is supplied, J-stationarity
  99derives the bridge relation with explicit remainder constant `n / 6`.
 100No hypothesis states a fact about `xRatio` or `log xRatio`. -/
 101theorem recognition_ratio_derived_of_deficit_source_coupling {H : Type*}
 102    (C : DeficitSourceConstitutiveCoupling H) (σ : H) :
 103    |Real.log ((ratioBridgeFromDeficitSourceCoupling C).xRatio σ)
 104        - C.kappa σ * C.geometricDeficit σ|
 105      ≤ (C.channels : ℝ) / 6 * C.meshScale ^ 3 :=
 106  (ratioBridgeFromDeficitSourceCoupling C).ratio_relation σ
 107
 108/-- **THEOREM (stationarity receipt).** The ratio in the conditional
 109derivation is the exponential of the total strain of the unique sourced
 110minimizer. -/
 111theorem deficitSourceCoupling_logRatio_eq_minimizer_strain {H : Type*}
 112    (C : DeficitSourceConstitutiveCoupling H) (σ : H) :
 113    Real.log ((ratioBridgeFromDeficitSourceCoupling C).xRatio σ)
 114      = ∑ i, sourcedMinimizer C.channels (C.sourceStrength σ) i := by
 115  rw [C.source_eq σ]
 116  exact ofStationarity_log_xRatio_eq_minimizer_strain C.channels
 117    C.channels_pos C.kappa C.geometricDeficit C.meshScale
 118    C.meshScale_pos
 119    (fun τ => by
 120      rw [← C.source_eq τ]
 121      exact C.source_dominated τ)
 122    σ
 123
 124/-! ## 3. The bare ledger cannot select the signed source -/
 125
 126/-- The bare two-cell ledger induced by the exact unit-coupled witness with
 127signed source parameter `d`. -/
 128noncomputable def signBlindBareLedger (d : ℝ) :
 129    RecognitionLedger.RecognitionLedger (Fin 2) :=
 130  ratioBridgeLedger (twoHingeWitnessBridge d)
 131
 132/-- Two recognition ledgers with the same cost function are equal (the
 133remaining fields are proofs). -/
 134private theorem recognitionLedger_cost_ext {Λ : Type*} [Fintype Λ]
 135    [DecidableEq Λ] {L L' : RecognitionLedger.RecognitionLedger Λ}
 136    (h : L.cost = L'.cost) : L = L' := by
 137  cases L
 138  cases L'
 139  subst h
 140  rfl
 141
 142/-- **THEOREM (same bare ledger, opposite signed source).** Reversing the
 143source orientation leaves every J-cost, hence the entire bare recognition
 144ledger, unchanged. -/
 145theorem signBlindBareLedger_neg_eq (d : ℝ) :
 146    signBlindBareLedger (-d) = signBlindBareLedger d := by
 147  apply recognitionLedger_cost_ext
 148  funext i j
 149  rw [show (signBlindBareLedger (-d)).cost i j
 150      = Cost.Jcost ((twoHingeWitnessBridge (-d)).xRatio i
 151          / (twoHingeWitnessBridge (-d)).xRatio j) from
 152        ratioBridgeLedger_cost (twoHingeWitnessBridge (-d)) i j]
 153  rw [show (signBlindBareLedger d).cost i j
 154      = Cost.Jcost ((twoHingeWitnessBridge d).xRatio i
 155          / (twoHingeWitnessBridge d).xRatio j) from
 156        ratioBridgeLedger_cost (twoHingeWitnessBridge d) i j]
 157  have hratio :
 158      (twoHingeWitnessBridge (-d)).xRatio i
 159          / (twoHingeWitnessBridge (-d)).xRatio j
 160        = ((twoHingeWitnessBridge d).xRatio i
 161            / (twoHingeWitnessBridge d).xRatio j)⁻¹ := by
 162    rw [twoHingeWitnessBridge_xRatio_neg d i,
 163      twoHingeWitnessBridge_xRatio_neg d j, inv_div_inv, inv_div]
 164  rw [hratio]
 165  exact (Cost.Jcost_symm
 166    (div_pos ((twoHingeWitnessBridge d).xRatio_pos i)
 167      ((twoHingeWitnessBridge d).xRatio_pos j))).symm
 168
 169/-- A proposed universal recovery of the signed unit-coupled source from a
 170bare two-cell ledger.  The next theorem proves that no such selector exists. -/
 171def RecoversSignedSourceFromBareLedger
 172    (select : RecognitionLedger.RecognitionLedger (Fin 2) → ℝ) : Prop :=
 173  ∀ d : ℝ, select (signBlindBareLedger d) = d
 174
 175/-- **THEOREM (the exact bare-ledger blocker).** No function of a bare
 176`RecognitionLedger (Fin 2)` can universally recover the signed source of
 177the exact unit-coupled witness family.  The ledgers at sources `1` and `-1`
 178are equal, while the required outputs are different.  Therefore signed
 179deficit-source orientation is extra constitutive data, not information
 180contained in the bare ledger. -/
 181theorem no_bare_ledger_selector_recovers_signed_source :
 182    ¬ ∃ select : RecognitionLedger.RecognitionLedger (Fin 2) → ℝ,
 183      RecoversSignedSourceFromBareLedger select := by
 184  rintro ⟨select, hselect⟩
 185  have hneg := hselect (-1)
 186  have hpos := hselect 1
 187  rw [signBlindBareLedger_neg_eq 1] at hneg
 188  norm_num at hneg hpos
 189  linarith
 190
 191/-! ## 4. A nontrivial source-backed family exists -/
 192
 193/-- **THEOREM (nontrivial source-backed family).** For every nonzero
 194coupling and positive channel count, the quadratic sourced family is
 195uniformly admissible.  Its source is exactly `n*h^2`, and at every nonzero
 196mesh both its geometric deficit and stationary log-ratio are nonzero.
 197Thus the conditional positive route is populated by a genuine small-mesh
 198family rather than a zero-source or fixed-mesh witness. -/
 199theorem nontrivial_source_backed_family_exists
 200    (n : ℕ) (hn : 1 ≤ n) (h₀ kappa : ℝ) (hκ : kappa ≠ 0) :
 201    ∃ F : RecognitionRatioFamily,
 202      F.IsAdmissible h₀ kappa ((n : ℝ) / |kappa|)
 203          ((n : ℝ) * h₀ ^ 3 / 6) ∧
 204      (∀ h, kappa * F.deficit h = (n : ℝ) * h ^ 2) ∧
 205      (∀ h, h ≠ 0 →
 206        F.deficit h ≠ 0 ∧ 0 < Real.log (F.ratio h)) := by
 207  refine ⟨quadraticSourceFamily n kappa,
 208    quadraticSourceFamily_isAdmissible n hn h₀ kappa hκ, ?_, ?_⟩
 209  · intro h
 210    show kappa * ((n : ℝ) / kappa * h ^ 2) = (n : ℝ) * h ^ 2
 211    field_simp
 212  · intro h hh
 213    exact ⟨quadraticSourceFamily_deficit_ne_zero n hn kappa h hκ hh,
 214      quadraticSourceFamily_logRatio_pos n hn kappa h hκ hh⟩
 215
 216/-! ## 5. Exact P2.1 terminal package -/
 217
 218/-- A proposition-valued certificate collecting the exact P2.1 terminal.
 219Unlike the historical status records, every field is mathematical content. -/
 220structure RecognitionRatioSubstrateBlockerCertificate : Prop where
 221  coboundary_cycle_telescope :
 222    ∀ {Λ : Type*} {s : Λ → Λ → ℝ}, IsCoboundary s →
 223      ∀ (v : ℕ → Λ) (m : ℕ), v m = v 0 →
 224        ∑ k ∈ Finset.range m, s (v k) (v (k + 1)) = 0
 225  imposed_budget_is_circular :
 226    ∀ {n : ℕ} (t : Fin n → ℝ) (kappa delta : ℝ),
 227      (∑ i, t i = kappa * delta) →
 228        naiveLogRatio n t = kappa * delta
 229  bare_ledger_cannot_recover_signed_source :
 230    ¬ ∃ select : RecognitionLedger.RecognitionLedger (Fin 2) → ℝ,
 231      RecoversSignedSourceFromBareLedger select
 232  coupling_derives_ratio :
 233    ∀ {H : Type*} (C : DeficitSourceConstitutiveCoupling H) (σ : H),
 234      |Real.log ((ratioBridgeFromDeficitSourceCoupling C).xRatio σ)
 235          - C.kappa σ * C.geometricDeficit σ|
 236        ≤ (C.channels : ℝ) / 6 * C.meshScale ^ 3
 237  nontrivial_source_family :
 238    ∀ (n : ℕ), 1 ≤ n → ∀ (h₀ kappa : ℝ), kappa ≠ 0 →
 239      ∃ F : RecognitionRatioFamily,
 240        F.IsAdmissible h₀ kappa ((n : ℝ) / |kappa|)
 241            ((n : ℝ) * h₀ ^ 3 / 6) ∧
 242        (∀ h, kappa * F.deficit h = (n : ℝ) * h ^ 2) ∧
 243        (∀ h, h ≠ 0 →
 244          F.deficit h ≠ 0 ∧ 0 < Real.log (F.ratio h))
 245
 246/-- **P2.1 HEADLINE THEOREM (strongest honest terminal).**
 247
 248The exact missing premise preventing `recognition_ratio_derived` from the
 249bare `RecognitionLedger` is `DeficitSourceConstitutiveCoupling`: a signed
 250source `c_sigma = kappa_sigma * delta_sigma` linearly coupled to total
 251strain in the J-cost action.  Coboundary circulation gives zero, an imposed
 252budget is circular, and the bare J-ledger cannot choose between opposite
 253source orientations.  With that named premise supplied, J-stationarity
 254derives the ratio bridge, and a nontrivial uniform source-backed family
 255exists. -/
 256theorem recognition_ratio_derived_bare_ledger_terminal :
 257    RecognitionRatioSubstrateBlockerCertificate where
 258  coboundary_cycle_telescope := by
 259    intro Λ s hs v m hcycle
 260    exact closedCycle_coboundary_sum_eq_zero hs v m hcycle
 261  imposed_budget_is_circular := by
 262    intro n t kappa delta hbudget
 263    exact budget_implies_ratio_without_stationarity t kappa delta hbudget
 264  bare_ledger_cannot_recover_signed_source :=
 265    no_bare_ledger_selector_recovers_signed_source
 266  coupling_derives_ratio := by
 267    intro H C σ
 268    exact recognition_ratio_derived_of_deficit_source_coupling C σ
 269  nontrivial_source_family := by
 270    intro n hn h₀ kappa hκ
 271    exact nontrivial_source_backed_family_exists n hn h₀ kappa hκ
 272
 273#print axioms recognition_ratio_derived_bare_ledger_terminal
 274#print axioms no_bare_ledger_selector_recovers_signed_source
 275#print axioms recognition_ratio_derived_of_deficit_source_coupling
 276#print axioms nontrivial_source_backed_family_exists
 277
 278end SevenGaps
 279end Gravity
 280end IndisputableMonolith
 281