IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D

   1import Mathlib
   2import IndisputableMonolith.Recognition
   3import IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioSubstrateBlocker
   4import IndisputableMonolith.Gravity.SevenGaps.LedgerEnergyBridge
   5
   6/-!
   7# Wave B residual R3: dual-entry signed-source enrichment (no xRatio)
   8
   9QG full-completion session, Wave B attack on
  10`TypedResidual_signed_source_enrichment_schema` from
  11`plans/QG_WaveB_Gap1_Residual_DAG_Draft_20260721.txt`.
  12
  13## Core idea
  14
  15The bare cost ledger `RecognitionLedger` is a derived shadow of the
  16foundational `Recognition.Ledger`, which carries two signed columns
  17`debit, credit : M.U → ℤ` with `phi = debit - credit`. The J-cost quotient
  18is even and forgets exactly `sign(phi)`. The R3 enrichment is therefore the
  19dual-entry column orientation: `DualEntryStrainState` with integer debit /
  20credit columns, nonnegative magnitude, and a unit-flux cap.
  21
  22## Convention (Z/2 pin)
  23
  24`deficit iff debit-leads` is one global ℤ/2 convention: the ledger mirror of
  25the Regge sign convention in `meshGeometricDeficit_regge_convention`.
  26Flipping the global convention swaps columns and negates `phi` / `strain`
  27while leaving the bare J-ledger unchanged (`toBare_swap`).
  28
  29## Honesty / scope
  30
  31* Does **not** flip `gap1_bridge_derived`.
  32* Does **not** bind the ledger-named `recognition_ratio_derived` Prop
  33  (that is R5 composition of the conditional theorem with a named binding).
  34* Carrier for later mesh assembly remains the reshaped `H = ℝ` from R1/R2,
  35  not an encoded Freudenthal triangulation.
  36* R0a/R0b (validation name-binding) remain open.
  37* Posting-run realization (F3 / `LedgerPostingAdjacency`) is omitted as
  38  garnish; load-bearing content is F2 + separation (a)(b)(c).
  39* Anchor hardening: `DualEntryStrainState.ofLedger` builds the enrichment
  40  from an actual foundational `Recognition.Ledger` on a discrete carrier
  41  structure (`discreteCarrier`), with `phi_ofLedger` and
  42  `enrichedWitness_eq_ofLedger` as theorems (not docstring citations).
  43
  44Vacuity guards: the only real-valued field is `mag` with `mag_nonneg`
  45(no signed real field); `flux_unit` caps orientation at one quantum; no
  46definition field mentions `xRatio`, `Real.log`, or `ratio_relation`
  47(`Real.log_exp` appears only in the toBare bridge lemma).
  48-/
  49
  50namespace IndisputableMonolith
  51namespace Gravity
  52namespace Analysis
  53namespace RecognitionDualEntryEnrichment4D
  54
  55open SevenGaps
  56open RecognitionLedger
  57open Recognition
  58
  59noncomputable section
  60
  61/-! ## §1. Dual-entry strain enrichment -/
  62
  63/-- **MODEL (R3 enrichment).** Dual-entry column orientation: integer debit
  64and credit columns, nonnegative magnitude, unit flux. Strain is the signed
  65product `(debit - credit) * mag`. No field mentions `xRatio` or `Real.log`. -/
  66structure DualEntryStrainState (Λ : Type*) where
  67  debit : Λ → ℤ
  68  credit : Λ → ℤ
  69  mag : Λ → ℝ
  70  mag_nonneg : ∀ i, 0 ≤ mag i
  71  flux_unit : ∀ i, |debit i - credit i| ≤ 1
  72
  73variable {Λ : Type*}
  74
  75/-- Column imbalance (foundational `Recognition.phi` shape). -/
  76def DualEntryStrainState.phi (S : DualEntryStrainState Λ) : Λ → ℤ :=
  77  fun i => S.debit i - S.credit i
  78
  79/-- Signed strain: integer orientation times nonnegative magnitude. -/
  80def DualEntryStrainState.strain (S : DualEntryStrainState Λ) : Λ → ℝ :=
  81  fun i => (S.phi i : ℝ) * S.mag i
  82
  83/-- Extracted signed source field (enrichment → carrier → ℝ). -/
  84def DualEntryStrainState.extract (S : DualEntryStrainState Λ) : Λ → ℝ :=
  85  S.strain
  86
  87/-- Bare J-cost ledger shadow (forgets sign via J-evenness). -/
  88noncomputable def DualEntryStrainState.toBare [Fintype Λ] [DecidableEq Λ]
  89    (S : DualEntryStrainState Λ) : RecognitionLedger Λ :=
  90  coboundaryStrainLedger S.strain
  91
  92/-- Swap debit and credit columns (ℤ/2 orientation reverse). -/
  93def DualEntryStrainState.swap (S : DualEntryStrainState Λ) :
  94    DualEntryStrainState Λ where
  95  debit := S.credit
  96  credit := S.debit
  97  mag := S.mag
  98  mag_nonneg := S.mag_nonneg
  99  flux_unit := by
 100    intro i
 101    have h := S.flux_unit i
 102    -- |credit - debit| = |debit - credit|
 103    simpa [abs_sub_comm] using h
 104
 105/-! ## §1b. Type-level anchor to foundational `Recognition.Ledger` -/
 106
 107/-- Discrete recognition structure on a finite carrier: units are `Λ`,
 108relation is total (carrier-only; no posting graph is used by the bridge).
 109`abbrev` so `(discreteCarrier Λ).U` reduces to `Λ` (RecognitionStructure
 110fixes universe `Type`, not `Type*`). -/
 111abbrev discreteCarrier (Λ : Type) : RecognitionStructure where
 112  U := Λ
 113  R := fun _ _ => True
 114
 115/-- **Type-level anchor.** Restrict a foundational `Recognition.Ledger` on
 116`discreteCarrier Λ` to a `DualEntryStrainState` by supplying a nonnegative
 117magnitude and a unit-flux hypothesis on `Recognition.phi`. -/
 118def DualEntryStrainState.ofLedger {Λ : Type}
 119    (L : Ledger (discreteCarrier Λ)) (mag : Λ → ℝ)
 120    (hmag : ∀ i, 0 ≤ mag i)
 121    (hflux : ∀ i, |Recognition.phi L i| ≤ 1) : DualEntryStrainState Λ where
 122  debit := L.debit
 123  credit := L.credit
 124  mag := mag
 125  mag_nonneg := hmag
 126  flux_unit := by
 127    intro i
 128    simpa [Recognition.phi] using hflux i
 129
 130/-- **THEOREM.** Column imbalance of `ofLedger` is the foundational
 131`Recognition.phi` on the discrete carrier. -/
 132theorem DualEntryStrainState.phi_ofLedger {Λ : Type}
 133    (L : Ledger (discreteCarrier Λ)) (mag : Λ → ℝ)
 134    (hmag : ∀ i, 0 ≤ mag i)
 135    (hflux : ∀ i, |Recognition.phi L i| ≤ 1) :
 136    (DualEntryStrainState.ofLedger L mag hmag hflux).phi =
 137      Recognition.phi L := by
 138  funext i
 139  simp only [DualEntryStrainState.phi, DualEntryStrainState.ofLedger,
 140    Recognition.phi]
 141
 142/-! ## §2. F2: swap negates signed data, preserves bare ledger -/
 143
 144theorem DualEntryStrainState.phi_swap (S : DualEntryStrainState Λ) :
 145    (S.swap).phi = fun i => -S.phi i := by
 146  funext i
 147  simp only [DualEntryStrainState.phi, DualEntryStrainState.swap]
 148  omega
 149
 150theorem DualEntryStrainState.strain_swap (S : DualEntryStrainState Λ) :
 151    (S.swap).strain = fun i => -S.strain i := by
 152  funext i
 153  have hφ : (S.swap).phi i = -S.phi i := congrFun S.phi_swap i
 154  have hmag : (S.swap).mag i = S.mag i := rfl
 155  simp only [DualEntryStrainState.strain, hφ, hmag, Int.cast_neg, neg_mul]
 156
 157/-- Two recognition ledgers with the same cost function are equal
 158(remaining fields are proofs). Local re-proof of the blocker's private
 159`recognitionLedger_cost_ext`. -/
 160theorem recognitionLedger_cost_ext {Λ' : Type*} [Fintype Λ'] [DecidableEq Λ']
 161    {L L' : RecognitionLedger Λ'} (h : L.cost = L'.cost) : L = L' := by
 162  cases L
 163  cases L'
 164  subst h
 165  rfl
 166
 167/-- **THEOREM (F2).** Column swap preserves the bare J-ledger
 168(mirrors `signBlindBareLedger_neg_eq` via J-cost evenness). -/
 169theorem DualEntryStrainState.toBare_swap [Fintype Λ] [DecidableEq Λ]
 170    (S : DualEntryStrainState Λ) :
 171    (S.swap).toBare = S.toBare := by
 172  apply recognitionLedger_cost_ext
 173  funext i j
 174  -- cost i j = Jcost (exp (strain i - strain j))
 175  change Cost.Jcost (Real.exp ((S.swap).strain i - (S.swap).strain j))
 176      = Cost.Jcost (Real.exp (S.strain i - S.strain j))
 177  have hswap : (S.swap).strain = fun k => -S.strain k := S.strain_swap
 178  rw [show (S.swap).strain i = -S.strain i from congrFun hswap i,
 179    show (S.swap).strain j = -S.strain j from congrFun hswap j]
 180  have hinv :
 181      Real.exp (-S.strain i - (-S.strain j))
 182        = (Real.exp (S.strain i - S.strain j))⁻¹ := by
 183    rw [← Real.exp_neg]
 184    congr 1
 185    ring
 186  rw [hinv]
 187  exact (Cost.Jcost_symm (Real.exp_pos _)).symm
 188
 189/-! ## §3. Enriched witness family (Fin 2) -/
 190
 191/-- Dual-entry witness realizing signed source `d` on two cells.
 192Debit-leads iff `0 ≤ d` (global ℤ/2 convention). Magnitude `|d|`. -/
 193noncomputable def enrichedWitness (d : ℝ) : DualEntryStrainState (Fin 2) where
 194  debit := fun σ =>
 195    if 0 ≤ d then (if σ = 0 then 1 else 0) else (if σ = 0 then 0 else 1)
 196  credit := fun σ =>
 197    if 0 ≤ d then (if σ = 0 then 0 else 1) else (if σ = 0 then 1 else 0)
 198  mag := fun _ => |d|
 199  mag_nonneg := fun _ => abs_nonneg d
 200  flux_unit := by
 201    intro σ
 202    by_cases hd : 0 ≤ d
 203    · simp [hd]
 204      by_cases hσ : σ = 0
 205      · simp [hσ]
 206      · simp [hσ]
 207    · simp [hd]
 208      by_cases hσ : σ = 0
 209      · simp [hσ]
 210      · simp [hσ]
 211
 212theorem enrichedWitness_strain (d : ℝ) :
 213    (enrichedWitness d).strain = fun σ => if σ = 0 then d else -d := by
 214  funext σ
 215  simp only [DualEntryStrainState.strain, DualEntryStrainState.phi,
 216    enrichedWitness]
 217  by_cases hd : 0 ≤ d
 218  · simp only [hd, ↓reduceIte]
 219    by_cases hσ : σ = 0
 220    · simp [hσ, abs_of_nonneg hd]
 221    · simp [hσ, abs_of_nonneg hd]
 222  · have hd' : d < 0 := lt_of_not_ge hd
 223    simp only [hd, ↓reduceIte]
 224    by_cases hσ : σ = 0
 225    · simp [hσ, abs_of_neg hd']
 226    · simp [hσ, abs_of_neg hd']
 227
 228theorem enrichedWitness_extract_zero (d : ℝ) :
 229    (enrichedWitness d).extract 0 = d := by
 230  simp [DualEntryStrainState.extract, enrichedWitness_strain d]
 231
 232/-- Foundational ledger whose columns realize `enrichedWitness d`. -/
 233def enrichedWitnessLedger (d : ℝ) : Ledger (discreteCarrier (Fin 2)) where
 234  debit := fun σ =>
 235    if 0 ≤ d then (if σ = 0 then 1 else 0) else (if σ = 0 then 0 else 1)
 236  credit := fun σ =>
 237    if 0 ≤ d then (if σ = 0 then 0 else 1) else (if σ = 0 then 1 else 0)
 238
 239theorem enrichedWitnessLedger_phi_abs_le_one (d : ℝ) (σ : Fin 2) :
 240    |Recognition.phi (enrichedWitnessLedger d) σ| ≤ 1 := by
 241  simp only [Recognition.phi, enrichedWitnessLedger]
 242  by_cases hd : 0 ≤ d
 243  · simp [hd]
 244    by_cases hσ : σ = 0
 245    · simp [hσ]
 246    · simp [hσ]
 247  · simp [hd]
 248    by_cases hσ : σ = 0
 249    · simp [hσ]
 250    · simp [hσ]
 251
 252/-- **THEOREM.** The enriched witness is the foundational ledger restricted
 253to the carrier with magnitude `|d|` (type-level factoring through
 254`ofLedger`). -/
 255theorem enrichedWitness_eq_ofLedger (d : ℝ) :
 256    enrichedWitness d =
 257      DualEntryStrainState.ofLedger (enrichedWitnessLedger d)
 258        (fun _ => |d|) (fun _ => abs_nonneg d)
 259        (enrichedWitnessLedger_phi_abs_le_one d) :=
 260  rfl
 261
 262/-- Bridge: enrichment bare shadow equals the blocker's sign-blind ledger. -/
 263theorem enrichedWitness_toBare (d : ℝ) :
 264    (enrichedWitness d).toBare = signBlindBareLedger d := by
 265  -- signBlindBareLedger d = coboundaryStrainLedger (log ∘ xRatio)
 266  -- and log (exp (if σ=0 then d else -d)) = if σ=0 then d else -d
 267  apply recognitionLedger_cost_ext
 268  funext i j
 269  change Cost.Jcost (Real.exp ((enrichedWitness d).strain i
 270      - (enrichedWitness d).strain j))
 271      = (signBlindBareLedger d).cost i j
 272  have hcost := ratioBridgeLedger_cost (twoHingeWitnessBridge d) i j
 273  -- Unfold signBlindBareLedger through ratioBridgeLedger
 274  have hsb :
 275      (signBlindBareLedger d).cost i j
 276        = Cost.Jcost ((twoHingeWitnessBridge d).xRatio i
 277            / (twoHingeWitnessBridge d).xRatio j) := hcost
 278  rw [hsb]
 279  -- strain = log ∘ xRatio of the witness
 280  have hlog :
 281      (fun σ : Fin 2 => Real.log ((twoHingeWitnessBridge d).xRatio σ))
 282        = (enrichedWitness d).strain := by
 283    funext σ
 284    simp only [twoHingeWitnessBridge, enrichedWitness_strain d]
 285    rw [Real.log_exp]
 286  -- coboundary cost from strain equals J(exp(Δ strain))
 287  -- and exp(log xRatio i - log xRatio j) = xRatio i / xRatio j
 288  have hstrain_i :
 289      (enrichedWitness d).strain i
 290        = Real.log ((twoHingeWitnessBridge d).xRatio i) := by
 291    rw [← hlog]
 292  have hstrain_j :
 293      (enrichedWitness d).strain j
 294        = Real.log ((twoHingeWitnessBridge d).xRatio j) := by
 295    rw [← hlog]
 296  rw [hstrain_i, hstrain_j, Real.exp_sub,
 297    Real.exp_log ((twoHingeWitnessBridge d).xRatio_pos i),
 298    Real.exp_log ((twoHingeWitnessBridge d).xRatio_pos j)]
 299
 300/-! ## §4. Separation: enrichment strictly richer than bare ledger -/
 301
 302/-- **(a)** The bare shadow is not injective on the enriched witness family. -/
 303theorem toBare_not_injective :
 304    (enrichedWitness (1 : ℝ)).toBare = (enrichedWitness (-1 : ℝ)).toBare ∧
 305      (enrichedWitness (1 : ℝ)).extract 0 ≠
 306        (enrichedWitness (-1 : ℝ)).extract 0 := by
 307  constructor
 308  · rw [enrichedWitness_toBare, enrichedWitness_toBare,
 309      signBlindBareLedger_neg_eq]
 310  · rw [enrichedWitness_extract_zero, enrichedWitness_extract_zero]
 311    norm_num
 312
 313/-- **(b) / Decoy 1.** Any α-valued observable that factors through `toBare`
 314is swap-even (invariant under column exchange). -/
 315theorem bare_factorable_is_swap_even {α : Type*}
 316    (f : DualEntryStrainState (Fin 2) → α)
 317    (select : RecognitionLedger (Fin 2) → α)
 318    (hf : ∀ E, f E = select E.toBare) (E : DualEntryStrainState (Fin 2)) :
 319    f E.swap = f E := by
 320  rw [hf, hf, DualEntryStrainState.toBare_swap]
 321
 322/-- Proposed recovery of the signed extract (hinge 0) from a bare ledger. -/
 323def RecoversExtractFromBare
 324    (select : RecognitionLedger (Fin 2) → ℝ) : Prop :=
 325  ∀ d : ℝ, select (enrichedWitness d).toBare = (enrichedWitness d).extract 0
 326
 327/-- **(c) THEOREM.** No bare-ledger selector recovers the enriched extract.
 328Direct reduction to `no_bare_ledger_selector_recovers_signed_source`. -/
 329theorem extract_not_bare_factorable :
 330    ¬ ∃ select : RecognitionLedger (Fin 2) → ℝ,
 331      RecoversExtractFromBare select := by
 332  rintro ⟨select, hselect⟩
 333  exact no_bare_ledger_selector_recovers_signed_source ⟨select, by
 334    intro d
 335    have h := hselect d
 336    rw [enrichedWitness_toBare d, enrichedWitness_extract_zero d] at h
 337    exact h⟩
 338
 339/-! ## §5. Typed residual R3 -/
 340
 341/-- **R3.** Signed-source enrichment strictly richer than bare
 342`RecognitionLedger`: dual-entry state with extract recovering the signed
 343witness source, bare shadow equal to `signBlindBareLedger`, and no bare
 344selector recovering extract. -/
 345def TypedResidual_signed_source_enrichment_schema : Prop :=
 346  (∀ d : ℝ, (enrichedWitness d).extract 0 = d) ∧
 347    (∀ d : ℝ, (enrichedWitness d).toBare = signBlindBareLedger d) ∧
 348      (∀ S : DualEntryStrainState (Fin 2), (S.swap).toBare = S.toBare) ∧
 349        ¬ ∃ select : RecognitionLedger (Fin 2) → ℝ,
 350          RecoversExtractFromBare select
 351
 352/-- **THEOREM:** R3 closed. -/
 353theorem typedResidual_signed_source_enrichment_schema_closed :
 354    TypedResidual_signed_source_enrichment_schema :=
 355  ⟨enrichedWitness_extract_zero, enrichedWitness_toBare,
 356    DualEntryStrainState.toBare_swap, extract_not_bare_factorable⟩
 357
 358theorem TypedResidual_signed_source_enrichment_schema_closed :
 359    TypedResidual_signed_source_enrichment_schema :=
 360  typedResidual_signed_source_enrichment_schema_closed
 361
 362/-! ## §6. Status (no ledger flag touch) -/
 363
 364structure RecognitionDualEntryEnrichment4DStatus where
 365  r3Closed : Bool
 366  postingRunRealizationDropped : Bool
 367  gap1BridgeDerived : Bool
 368
 369def recognitionDualEntryEnrichment4DStatus :
 370    RecognitionDualEntryEnrichment4DStatus where
 371  r3Closed := true
 372  postingRunRealizationDropped := true
 373  gap1BridgeDerived := false
 374
 375theorem recognitionDualEntryEnrichment4DStatus_flags :
 376    recognitionDualEntryEnrichment4DStatus.r3Closed = true ∧
 377      recognitionDualEntryEnrichment4DStatus.postingRunRealizationDropped =
 378        true ∧
 379        recognitionDualEntryEnrichment4DStatus.gap1BridgeDerived = false := by
 380  decide
 381
 382end
 383
 384end RecognitionDualEntryEnrichment4D
 385end Analysis
 386end Gravity
 387end IndisputableMonolith
 388