IndisputableMonolith.Verification.T5.LedgerCost

   1import Mathlib
   2import IndisputableMonolith.Recognition
   3import IndisputableMonolith.RecogSpec.Core
   4-- Note: LedgerNecessity.lean has pre-existing build issues; we don't need it directly
   5-- The ledger structure is defined independently here for the T5 forcing argument
   6
   7/-!
   8# Ledger-Derived Cost Constraints (Symmetry and Unit) — with a No-Go Certificate
   9
  10This module derives TWO of the T5 constraints from the ledger structure (T3),
  11and proves that the remaining constraint CANNOT be so derived.
  12
  13## Main Results
  14
  151. **Symmetry Forced**: The ledger's double-entry structure forces F(x) = F(1/x).
  162. **Unit Forced**: The identity posting (no change) has zero cost, forcing F(1) = 0.
  173. **NO-GO (`aczel_hypothesis_refuted`)**: symmetry + unit + continuity +
  18   curvature calibration do NOT force the Cosh-Add (d'Alembert) identity.
  19   Witness: `G(t) = t²/2`. The composition law C6 is an independent,
  20   load-bearing hypothesis of the T5 characterization theorem.
  21
  22## The Honest Chain
  23
  24```
  25T3 (Ledger Structure)
  26  ↓ [Double-entry bookkeeping]
  27F(x) = F(1/x)  (Reciprocal Symmetry — proved here)
  28  ↓ [Identity posting = no entry]
  29F(1) = 0  (Unit Normalization — proved here)
  30
  31C6 (composition / Cosh-Add)  — INDEPENDENT HYPOTHESIS (not derivable; no-go proved here)
  32C7 (calibration λ = 1)       — normalization choice
  33  ↓ [given C1–C7: Aczél-type classification]
  34T5: J(x) = ½(x + 1/x) - 1 is the unique admissible cost
  35```
  36
  37## History
  38
  39An earlier revision of this file claimed the Cosh-Add identity followed from
  40the ledger constraints plus continuity, citing Aczél (1966, Thm. 3.1.3), and
  41concluded T5 was "unconditionally forced" from T1–T4. Both claims were false
  42(2026 internal audit, Finding 2) and are retracted; the refutation is now a
  43kernel-checked theorem in this file.
  44
  45## References
  46
  47- Aczél, J. "Lectures on Functional Equations and Their Applications" (1966), Ch. 3
  48  (classification of d'Alembert solutions — used with, not instead of, C6)
  49- Recognition Science: T3 Ledger Necessity theorems
  50
  51-/
  52
  53namespace IndisputableMonolith
  54namespace Verification
  55namespace T5
  56namespace LedgerCost
  57
  58open Real
  59
  60/-! ## Part 1: Ledger-Derived Cost Structure
  61
  62A ledger is a double-entry system where every debit has a matching credit.
  63The "cost" of a recognition event is the magnitude of the ledger entry required
  64to record the transition from state A to state B.
  65-/
  66
  67/-- A ledger posting records a transition between two positive values.
  68    The ratio A/B captures the "exchange rate" of the transition. -/
  69structure LedgerPosting where
  70  source : ℝ
  71  target : ℝ
  72  source_pos : 0 < source
  73  target_pos : 0 < target
  74
  75/-- The ratio of a ledger posting. -/
  76noncomputable def LedgerPosting.ratio (p : LedgerPosting) : ℝ :=
  77  p.source / p.target
  78
  79/-- The inverse posting (swapping source and target). -/
  80def LedgerPosting.inverse (p : LedgerPosting) : LedgerPosting :=
  81  { source := p.target
  82  , target := p.source
  83  , source_pos := p.target_pos
  84  , target_pos := p.source_pos }
  85
  86lemma LedgerPosting.inverse_ratio (p : LedgerPosting) :
  87    p.inverse.ratio = p.ratio⁻¹ := by
  88  simp only [inverse, ratio]
  89  have hs : p.source ≠ 0 := p.source_pos.ne'
  90  have ht : p.target ≠ 0 := p.target_pos.ne'
  91  field_simp
  92
  93/-- The identity posting (source = target). -/
  94noncomputable def LedgerPosting.identity (x : ℝ) (hx : 0 < x) : LedgerPosting :=
  95  { source := x
  96  , target := x
  97  , source_pos := hx
  98  , target_pos := hx }
  99
 100lemma LedgerPosting.identity_ratio (x : ℝ) (hx : 0 < x) :
 101    (LedgerPosting.identity x hx).ratio = 1 := by
 102  simp only [identity, ratio]
 103  have hne : x ≠ 0 := hx.ne'
 104  field_simp
 105
 106/-! ## Part 2: The Ledger Cost Functional
 107
 108The cost of a ledger posting measures the "work" required to record the transition.
 109This is defined in terms of the ratio, capturing the asymmetry between source and target.
 110-/
 111
 112/-- A cost functional on ledger postings.
 113
 114Note: an earlier revision carried a vacuous field `domain : ∀ x, 0 < x → True`
 115(flagged in external audit as contentless debris). It has been removed; the
 116positivity of ratios is enforced at the `LedgerPosting` level, not here. -/
 117structure LedgerCostFunctional where
 118  /-- The cost function on positive ratios. -/
 119  cost : ℝ → ℝ
 120
 121/-- The cost of a ledger posting under a cost functional. -/
 122noncomputable def LedgerCostFunctional.postingCost
 123    (F : LedgerCostFunctional) (p : LedgerPosting) : ℝ :=
 124  F.cost p.ratio
 125
 126/-! ## Part 3: Symmetry Forced from Double-Entry
 127
 128**Theorem**: In a double-entry ledger, the cost of posting A→B equals the cost of B→A.
 129
 130**Proof**: A double-entry ledger records both sides of every transaction:
 131- Posting A→B creates a debit of A and credit of B
 132- Posting B→A creates a debit of B and credit of A
 133- These are the same transaction viewed from opposite sides
 134- Therefore the cost must be equal
 135
 136In ratio terms: F(A/B) = F(B/A) = F((A/B)⁻¹)
 137-/
 138
 139/-- A cost functional respects double-entry if inverse postings have equal cost. -/
 140def LedgerCostFunctional.respectsDoubleEntry (F : LedgerCostFunctional) : Prop :=
 141  ∀ p : LedgerPosting, F.postingCost p = F.postingCost p.inverse
 142
 143/-- **Theorem (Symmetry Forced)**: Double-entry structure forces reciprocal symmetry.
 144
 145This is the key theorem connecting T3 (Ledger) to the T5 constraint F(x) = F(1/x).
 146-/
 147theorem symmetry_forced_from_double_entry
 148    (F : LedgerCostFunctional)
 149    (hDE : F.respectsDoubleEntry) :
 150    ∀ x, 0 < x → F.cost x = F.cost x⁻¹ := by
 151  intro x hx
 152  -- Construct a posting with ratio x
 153  let p : LedgerPosting := {
 154    source := x
 155    target := 1
 156    source_pos := hx
 157    target_pos := one_pos
 158  }
 159  -- The posting has ratio x
 160  have hp_ratio : p.ratio = x := by simp [LedgerPosting.ratio, p]
 161  -- The inverse posting has ratio 1/x
 162  have hp_inv_ratio : p.inverse.ratio = x⁻¹ := by
 163    rw [LedgerPosting.inverse_ratio, hp_ratio]
 164  -- By double-entry, costs are equal
 165  have h := hDE p
 166  simp only [LedgerCostFunctional.postingCost] at h
 167  rw [hp_ratio, hp_inv_ratio] at h
 168  exact h
 169
 170/-! ## Part 4: Unit Normalization Forced from Identity
 171
 172**Theorem**: The identity posting (no change) has zero cost.
 173
 174**Proof**: An identity posting A→A represents "no transaction" in the ledger.
 175No debit or credit is recorded. The cost of doing nothing must be zero,
 176as it's the baseline against which all other costs are measured.
 177
 178In ratio terms: F(1) = 0
 179-/
 180
 181/-- A cost functional has zero identity cost if F(1) = 0. -/
 182def LedgerCostFunctional.zeroIdentityCost (F : LedgerCostFunctional) : Prop :=
 183  F.cost 1 = 0
 184
 185/-- **Theorem (Unit Forced)**: Identity postings have zero cost.
 186
 187This is the key theorem connecting T3 (Ledger) to the T5 constraint F(1) = 0.
 188
 189The argument: An identity posting records no change in the ledger.
 190Since no entry is made, the cost must be zero.
 191-/
 192theorem unit_forced_from_identity_posting
 193    (F : LedgerCostFunctional)
 194    (hZero : ∀ p : LedgerPosting, p.source = p.target → F.postingCost p = 0) :
 195    F.zeroIdentityCost := by
 196  unfold LedgerCostFunctional.zeroIdentityCost
 197  -- Construct an identity posting
 198  let p := LedgerPosting.identity 1 one_pos
 199  have hp_eq : p.source = p.target := rfl
 200  have hp_ratio : p.ratio = 1 := LedgerPosting.identity_ratio 1 one_pos
 201  -- Apply the hypothesis
 202  have h := hZero p hp_eq
 203  simp only [LedgerCostFunctional.postingCost, hp_ratio] at h
 204  exact h
 205
 206/-! ## Part 5: Additivity from Sequential Postings
 207
 208**Theorem**: Sequential ledger postings have additive costs in log-space.
 209
 210**Proof**: If we post A→B and then B→C, the total ledger effect is A→C.
 211The costs should combine: Cost(A→B) + Cost(B→C) relates to Cost(A→C).
 212
 213In log-space (t = log(ratio)):
 214- Posting with ratio r₁ followed by ratio r₂ gives total ratio r₁·r₂
 215- log(r₁·r₂) = log(r₁) + log(r₂)
 216- This additivity in log-space constrains the functional form
 217
 218This property, combined with symmetry and continuity, leads to the cosh-add identity.
 219-/
 220
 221/-- Sequential postings: if p₁ goes A→B and p₂ goes B→C, the composition goes A→C. -/
 222def LedgerPosting.compose (p₁ p₂ : LedgerPosting)
 223    (h : p₁.target = p₂.source) : LedgerPosting :=
 224  { source := p₁.source
 225  , target := p₂.target
 226  , source_pos := p₁.source_pos
 227  , target_pos := p₂.target_pos }
 228
 229lemma LedgerPosting.compose_ratio (p₁ p₂ : LedgerPosting) (h : p₁.target = p₂.source) :
 230    (p₁.compose p₂ h).ratio = p₁.ratio * p₂.ratio := by
 231  simp only [compose, ratio]
 232  have ht1 : p₁.target ≠ 0 := p₁.target_pos.ne'
 233  have ht2 : p₂.target ≠ 0 := p₂.target_pos.ne'
 234  have hs2 : p₂.source ≠ 0 := p₂.source_pos.ne'
 235  rw [h]
 236  field_simp
 237
 238/-- In log-space, composition corresponds to addition of log-ratios. -/
 239lemma log_ratio_additive (p₁ p₂ : LedgerPosting) (h : p₁.target = p₂.source) :
 240    Real.log (p₁.compose p₂ h).ratio = Real.log p₁.ratio + Real.log p₂.ratio := by
 241  rw [LedgerPosting.compose_ratio p₁ p₂ h]
 242  have hr1 : 0 < p₁.ratio := by
 243    simp only [LedgerPosting.ratio]
 244    exact div_pos p₁.source_pos p₁.target_pos
 245  have hr2 : 0 < p₂.ratio := by
 246    simp only [LedgerPosting.ratio]
 247    exact div_pos p₂.source_pos p₂.target_pos
 248  exact Real.log_mul hr1.ne' hr2.ne'
 249
 250/-! ## Part 6: The Complete Forcing Theorem
 251
 252We now state the complete theorem: the ledger structure forces all T5 constraints
 253except the Cosh-Add identity, which follows from functional equation theory.
 254-/
 255
 256/-- A cost functional is ledger-compatible if it respects double-entry and
 257    has zero identity cost. -/
 258structure LedgerCompatible (F : LedgerCostFunctional) : Prop where
 259  double_entry : F.respectsDoubleEntry
 260  zero_identity : ∀ p : LedgerPosting, p.source = p.target → F.postingCost p = 0
 261
 262/-- **Main Theorem**: Ledger compatibility forces the T5 constraints.
 263
 264From the ledger structure (T3), we derive:
 2651. Reciprocal symmetry: F(x) = F(1/x)
 2662. Unit normalization: F(1) = 0
 267
 268These are the two physical constraints of T5. The remaining constraint
 269(the Cosh-Add identity, i.e. the composition law C6) is an INDEPENDENT
 270hypothesis: it does not follow from these constraints plus continuity
 271(see `aczel_hypothesis_refuted` below).
 272-/
 273theorem ledger_forces_t5_constraints
 274    (F : LedgerCostFunctional)
 275    (hLC : LedgerCompatible F) :
 276    (∀ x, 0 < x → F.cost x = F.cost x⁻¹) ∧ F.cost 1 = 0 := by
 277  constructor
 278  · exact symmetry_forced_from_double_entry F hLC.double_entry
 279  · exact unit_forced_from_identity_posting F hLC.zero_identity
 280
 281/-! ## Part 7: The Cosh-Add Identity Is an Independent Hypothesis (corrected)
 282
 283An earlier revision of this section claimed the Cosh-Add identity is "a
 284mathematical consequence of the constraints derived above plus continuity",
 285citing Aczél (1966, Theorem 3.1.3). **That claim was false** and is
 286retracted (2026 internal audit, Finding 2). Aczél's theorem classifies the
 287solutions OF the d'Alembert equation; it does not derive the equation from
 288evenness, normalization, continuity, and calibration. The counterexample
 289`G(t) = t²/2` (below) satisfies all four conditions and violates Cosh-Add.
 290
 291The honest status: Cosh-Add is the log-axis form of the composition law
 292(closure hypothesis C6 in the RS_v1 paper) and enters as an independent,
 293load-bearing hypothesis of the T5 characterization theorem.
 294-/
 295
 296/-- The Cosh-Add (d'Alembert-type) identity in the form used by T5.
 297
 298This is the log-axis form of the composition law C6. It is an INDEPENDENT
 299hypothesis of the T5 characterization: it is NOT implied by symmetry, unit
 300normalization, continuity, and curvature calibration (see
 301`aczel_hypothesis_refuted`).
 302-/
 303def CoshAddFromLedger (G : ℝ → ℝ) : Prop :=
 304  ∀ t u : ℝ, G (t+u) + G (t-u) = 2 * (G t * G u) + 2 * (G t + G u)
 305
 306/-- **REFUTED PROPOSITION** (retained only so its refutation can be stated).
 307
 308This proposition asserts that evenness + normalization + continuity + unit
 309log-curvature alone force the Cosh-Add (d'Alembert) identity. **It is FALSE.**
 310The quadratic cost `G(t) = t²/2` satisfies every hypothesis and violates
 311Cosh-Add (see `aczel_hypothesis_refuted` below).
 312
 313An earlier revision of this file misattributed this proposition to Aczél
 314(1966, Theorem 3.1.3) and presented it as established mathematics. That was
 315an error, identified in the 2026 internal audit (Thapa, T−2..T5 forcing
 316report, Finding 2). Aczél's classification runs in the OTHER direction: it
 317classifies solutions OF the d'Alembert equation; it does not derive the
 318equation from regularity hypotheses. The composition law (the paper's
 319closure hypothesis C6) is genuinely load-bearing and cannot be obtained
 320from symmetry, normalization, continuity, and calibration alone.
 321
 322Nothing in this repository may assume this proposition. It is kept as a
 323`def` solely as the subject of the no-go certificate below. -/
 324def aczel_theorem_3_1_3_hypothesis : Prop :=
 325  ∀ (G : ℝ → ℝ),
 326    Function.Even G →
 327    G 0 = 0 →
 328    Continuous G →
 329    deriv (deriv G) 0 = 1 →
 330    CoshAddFromLedger G
 331
 332/-- The quadratic-cost witness `G(t) = t²/2`. Even, vanishes at 0, continuous,
 333with unit second derivative at the origin — yet it does not satisfy Cosh-Add. -/
 334noncomputable def quadraticWitness : ℝ → ℝ := fun t => t ^ 2 / 2
 335
 336lemma quadraticWitness_even : Function.Even quadraticWitness := by
 337  intro t; simp [quadraticWitness]
 338
 339lemma quadraticWitness_zero : quadraticWitness 0 = 0 := by
 340  simp [quadraticWitness]
 341
 342lemma quadraticWitness_continuous : Continuous quadraticWitness := by
 343  unfold quadraticWitness; fun_prop
 344
 345lemma quadraticWitness_deriv : deriv quadraticWitness = fun t => t := by
 346  funext x
 347  have h : HasDerivAt quadraticWitness x x := by
 348    have := (hasDerivAt_pow 2 x).div_const 2
 349    simpa [quadraticWitness, pow_one] using this
 350  simpa using h.deriv
 351
 352lemma quadraticWitness_second_deriv : deriv (deriv quadraticWitness) 0 = 1 := by
 353  rw [quadraticWitness_deriv]
 354  simp
 355
 356/-- The witness violates Cosh-Add at t = u = 1: LHS = 2, RHS = 5/2. -/
 357lemma quadraticWitness_not_coshAdd : ¬ CoshAddFromLedger quadraticWitness := by
 358  intro h
 359  have h11 := h 1 1
 360  norm_num [quadraticWitness] at h11
 361
 362/-- **NO-GO CERTIFICATE (Finding 2 resolution)**: the proposition
 363`aczel_theorem_3_1_3_hypothesis` is false. Symmetry, unit normalization,
 364continuity, and unit log-curvature calibration do NOT force the Cosh-Add
 365identity; the composition law C6 is an independent, load-bearing hypothesis.
 366
 367Witness: `G(t) = t²/2`. -/
 368theorem aczel_hypothesis_refuted : ¬ aczel_theorem_3_1_3_hypothesis := by
 369  intro h
 370  exact quadraticWitness_not_coshAdd
 371    (h quadraticWitness quadraticWitness_even quadraticWitness_zero
 372      quadraticWitness_continuous quadraticWitness_second_deriv)
 373
 374/-! ## Summary (corrected 2026-07-06)
 375
 376What this file actually establishes:
 377
 378```
 379T3 (Ledger)  →  Symmetry F(x) = F(1/x)   (from double-entry, proved above)
 380             →  Unit F(1) = 0            (from identity posting, proved above)
 381```
 382
 383What it does NOT establish, and what `aczel_hypothesis_refuted` proves CANNOT
 384be established from these constraints alone:
 385
 386```
 387Symmetry + Unit + Continuity + Calibration  ↛  Cosh-Add  ↛  J
 388```
 389
 390The Cosh-Add (d'Alembert) identity is equivalent to the composition law
 391(the paper's closure hypothesis C6) and must be assumed or motivated
 392independently. The witness `G(t) = t²/2` satisfies every ledger-derived
 393constraint plus continuity and calibration, and is not J.
 394
 395Consequently T5 is a CONDITIONAL characterization theorem: given C1–C7
 396(including the load-bearing C6 and the calibration C7), J is the unique
 397cost. It is NOT unconditionally forced from T1–T4. An earlier revision of
 398this summary claimed otherwise; that claim is retracted, and the refutation
 399is now a kernel-checked certificate in this file.
 400-/
 401
 402end LedgerCost
 403end T5
 404end Verification
 405end IndisputableMonolith
 406