IndisputableMonolith.Gravity.SevenGaps.Gap5PhysicalMomentum

   1import IndisputableMonolith.Gravity.SevenGaps.Gap5NetImbalanceDerivation
   2
   3/-!
   4# Physical momentum from posting structure (MODEL)
   5
   6**Verdict, stated first.** Route **(c) LANDED**. A library-wide search of the
   7A1/Gap5 posting-dynamics modules, the ledger chart carrier, and the B1
   8siblings finds **no** existing posting-grounded definition of physical
   9momentum: every prior module treats `p : LedgerState → ℝ` as an abstract
  10observable with properties. The honest move is therefore to **define** the
  11physical momentum from posting data and prove the two remaining obligations
  12for that definition.
  13
  14## The definition (MODEL, posting-grounded)
  15
  16A double-entry posting contributes a debit column and a credit column. The
  17ledger state is the pair `(d, c)`. The net charge of that state is the signed
  18difference of the two columns:
  19
  20    physicalMomentum z := z.1 - z.2
  21
  22This is definitionally the library `imbalance`. The definition mentions only
  23posting/ledger column data. It does **not** mention additivity, Cauchy,
  24`EnergyEqualsCost`, or the kinetic condition. Those are theorems about the
  25definition, not inputs to it.
  26
  27## Obligations discharged
  28
  29* **(O1)** `PostingIncidence physicalMomentum`:
  30  `p(d,c) = p(d,0) + p(0,c)` holds by the arithmetic of net charge
  31  (`d - c = (d - 0) + (0 - c)`).
  32* **(O2)** `AdditiveOnDebitAxis physicalMomentum`:
  33  `f(m) := p(m,0)` is the identity on the debit axis, so
  34  `f(m+n) = f(m) + f(n)` holds because consolidation of pure-debit net charges
  35  adds the counts.
  36
  37With the already-proved consumer
  38`energyEqualsCost_of_posting_incidence_additive_unit`, continuity and unit
  39normalization of `physicalMomentum` (both theorems, no hypotheses) discharge
  40`EnergyEqualsCost physicalMomentum`. The chain from posting net charge to
  41`EnergyEqualsCost` therefore composes end-to-end for this defined `p`.
  42
  43## What is NOT claimed
  44
  45* No derivation of O1/O2 for an *arbitrary* abstract observable. The prior
  46  module's `cubeDiff` witness already shows that column incidence alone does
  47  not force the debit-axis Cauchy property
  48  (`N-route-qg-p1-p2-from-incidence-alone`). Defining the physical momentum as
  49  the net charge *selects* among column-separable observables.
  50* No flag flip. Flags 6 and 12 now rest on acceptance of this MODEL
  51  identification (physical momentum is the net charge of the double-entry
  52  ledger state), not on an undischarged quantified property of an abstract `p`.
  53* No use of `KineticCondition`, B1 kinetic-conditional additivity, or
  54  `EnergyEqualsCost` as a hypothesis. Those appear only as conclusions.
  55-/
  56
  57namespace IndisputableMonolith
  58namespace Gravity
  59namespace SevenGaps
  60namespace PhysicalMomentum
  61
  62open ChartFromLedgerMomentum MomentumAdditivity MomentumAdditivityComposition
  63open MomentumMagnitudeBridge EnergyEqualsCostDerivation NetImbalanceDerivation
  64
  65noncomputable section
  66
  67/-! ## §0. Inventory: no prior posting-grounded definition
  68
  69The Gap5 chain modules (`Gap5ChartFromLedgerMomentum`,
  70`Gap5MomentumAdditivity`, `Gap5MomentumMagnitudeBridge`,
  71`Gap5EnergyEqualsCostDerivation`, `Gap5MomentumAdditivityComposition`,
  72`Gap5NetImbalanceDerivation`) all quantify over an abstract
  73`p : LedgerState → ℝ`. The chart carrier supplies `imbalance` as a *candidate*
  74linear functional, not as a declared physical-momentum definition. The Gap2
  75posting-dynamics modules define incidence/counts on posting alphabets, not a
  76chart-level momentum observable. This module supplies the missing definition.
  77-/
  78
  79/-! ## §1. MODEL definition: physical momentum is net charge -/
  80
  81/-- **Physical momentum (FOUNDATIONAL MODEL, adopted by Jon 2026-07-31,
  82`D-qg-eec-adopted-as-model-20260731`).** The signed net charge of a
  83double-entry ledger state: debit column minus credit column. Posting-grounded:
  84every posting contributes to exactly these two columns, and the momentum
  85generated by the posting layer is their signed difference. Equal by definition
  86to the library `imbalance`.
  87
  88Adopted as a foundational MODEL, not derived: the wall theorem
  89`MomentumBridge.bridge_not_forced_by_scale_free_package` shows that no
  90conjunction of scale-free selection properties forces the momentum scale, so
  91the identification is an adoption, and the conversion-theorem lane (deriving
  92the scale from posting dynamics) stays OPEN frontier. The conditional-chain
  93assembly that discharges the bridge hypotheses against this identification
  94lives in `Gap5MomentumModelAssembly`. -/
  95def physicalMomentum : LedgerState → ℝ := imbalance
  96
  97theorem physicalMomentum_eq_imbalance :
  98    physicalMomentum = imbalance := rfl
  99
 100theorem physicalMomentum_def (z : LedgerState) :
 101    physicalMomentum z = z.1 - z.2 := rfl
 102
 103/-! ## §2. (O1) Posting incidence from the net-charge definition -/
 104
 105/-- **(O1).** Column posting incidence holds for the physical momentum because
 106net charge splits over the two axes: `d - c = (d - 0) + (0 - c)`. No abstract
 107incidence hypothesis: the property is a theorem about the definition. -/
 108theorem physicalMomentum_posting_incidence :
 109    PostingIncidence physicalMomentum := by
 110  intro d c
 111  change d - c = (d - 0) + (0 - c)
 112  ring
 113
 114/-! ## §3. (O2) Debit-axis Cauchy from consolidation of net charges -/
 115
 116/-- On the pure-debit axis the physical momentum is the identity: a pure-debit
 117state of charge `m` has net charge `m`. -/
 118theorem physicalMomentum_on_debit_axis (m : ℝ) :
 119    physicalMomentum (m, 0) = m := by
 120  change m - 0 = m
 121  ring
 122
 123/-- **(O2).** Debit-axis additivity: consolidating two pure-debit net charges
 124adds the counts. Immediate from the identity reading on the debit axis. -/
 125theorem physicalMomentum_additiveOnDebitAxis :
 126    AdditiveOnDebitAxis physicalMomentum := by
 127  intro m n
 128  rw [physicalMomentum_on_debit_axis m, physicalMomentum_on_debit_axis n,
 129    physicalMomentum_on_debit_axis (m + n)]
 130
 131/-- Net-imbalance reading is immediate: the momentum *is* the net charge. -/
 132theorem physicalMomentum_readsNetImbalance :
 133    ReadsNetImbalance physicalMomentum := by
 134  intro z
 135  change z.1 - z.2 = (z.1 - z.2) - 0
 136  ring
 137
 138theorem physicalMomentum_swap_odd : SwapOdd physicalMomentum := by
 139  intro z
 140  change z.2 - z.1 = -(z.1 - z.2)
 141  ring
 142
 143theorem physicalMomentum_continuous : Continuous physicalMomentum :=
 144  continuous_imbalance
 145
 146theorem physicalMomentum_unit :
 147    physicalMomentum (1, 0) ^ 2 = 1 := by
 148  change ((1 : ℝ) - 0) ^ 2 = 1
 149  norm_num
 150
 151theorem physicalMomentum_balance_vanishing :
 152    ∀ z : LedgerState, Balanced z → physicalMomentum z = 0 := by
 153  intro z hz
 154  change z.1 - z.2 = 0
 155  exact sub_eq_zero.mpr hz
 156
 157theorem physicalMomentum_additive :
 158    ∀ z w : LedgerState,
 159      physicalMomentum (z + w) = physicalMomentum z + physicalMomentum w := by
 160  intro z w
 161  change (z.1 + w.1) - (z.2 + w.2) = (z.1 - z.2) + (w.1 - w.2)
 162  ring
 163
 164/-! ## §4. End-to-end composition: EnergyEqualsCost for the defined p -/
 165
 166/-- **End-to-end discharge.** For the posting-grounded physical momentum, O1,
 167O2, continuity, and unit are all theorems (no remaining hypotheses). The
 168upstream consumer therefore yields full consolidation additivity,
 169balance-vanishing, and `EnergyEqualsCost`. -/
 170theorem energyEqualsCost_of_physicalMomentum :
 171    (∀ z w : LedgerState,
 172      physicalMomentum (z + w) =
 173        physicalMomentum z + physicalMomentum w) ∧
 174      (∀ z : LedgerState, Balanced z → physicalMomentum z = 0) ∧
 175      EnergyEqualsCost physicalMomentum :=
 176  energyEqualsCost_of_posting_incidence_additive_unit
 177    physicalMomentum
 178    physicalMomentum_posting_incidence
 179    physicalMomentum_swap_odd
 180    physicalMomentum_additiveOnDebitAxis
 181    physicalMomentum_continuous
 182    physicalMomentum_unit
 183
 184/-- Direct inhabitation of the full posting package (no hypotheses). -/
 185theorem physicalMomentum_inhabits_posting_package :
 186    PostingIncidence physicalMomentum ∧
 187      SwapOdd physicalMomentum ∧
 188      ReadsNetImbalance physicalMomentum ∧
 189      AdditiveOnDebitAxis physicalMomentum ∧
 190      Continuous physicalMomentum ∧
 191      physicalMomentum ((1, 0) : LedgerState) ^ 2 = 1 ∧
 192      EnergyEqualsCost physicalMomentum :=
 193  ⟨physicalMomentum_posting_incidence, physicalMomentum_swap_odd,
 194    physicalMomentum_readsNetImbalance, physicalMomentum_additiveOnDebitAxis,
 195    physicalMomentum_continuous, physicalMomentum_unit,
 196    (energyEqualsCost_of_physicalMomentum).2.2⟩
 197
 198/-! ## §5. Selection among column-separable observables (scoped witness)
 199
 200`cubeDiff` from the prior module is continuous, swap-odd, balance-vanishing,
 201unit-normalized, and column-incident, yet fails O2. It is a function of the
 202ledger columns but is **not** the net-charge reading. Quantifier first: this
 203is a concrete package witness on the stated `LedgerState` carrier, not a class
 204theorem over posting systems (`L-qg-witness-is-not-a-class-20260729`). The
 205MODEL definition selects the net-charge reading among column-separable
 206candidates; without that selection, O2 is not forced.
 207-/
 208
 209theorem cubeDiff_is_not_physicalMomentum :
 210    cubeDiff ≠ physicalMomentum := by
 211  intro h
 212  have h1 := congrFun h ((2, 1) : LedgerState)
 213  -- cubeDiff (2,1) = 8 - 1 = 7; physicalMomentum (2,1) = 1
 214  change (2 : ℝ) ^ 3 - (1 : ℝ) ^ 3 = (2 : ℝ) - 1 at h1
 215  norm_num at h1
 216
 217theorem net_charge_selected_among_incident :
 218    PostingIncidence physicalMomentum ∧
 219      AdditiveOnDebitAxis physicalMomentum ∧
 220      PostingIncidence cubeDiff ∧
 221      ¬ AdditiveOnDebitAxis cubeDiff ∧
 222      cubeDiff ≠ physicalMomentum :=
 223  ⟨physicalMomentum_posting_incidence, physicalMomentum_additiveOnDebitAxis,
 224    cubeDiff_posting_incidence, cubeDiff_not_additiveOnDebitAxis,
 225    cubeDiff_is_not_physicalMomentum⟩
 226
 227/-! ## §6. Certificate -/
 228
 229/-- **Physical-momentum MODEL verdict.** (c): `physicalMomentum` is defined as
 230the net charge of the double-entry ledger state; O1 and O2 are theorems about
 231that definition; the EnergyEqualsCost consumer fires with no remaining
 232hypotheses. Supporting selection witness: `cubeDiff` shares column incidence
 233and fails O2, so the net-charge identification is load-bearing. -/
 234structure PhysicalMomentumVerdict : Prop where
 235  definition_eq_imbalance : physicalMomentum = imbalance
 236  o1_posting_incidence : PostingIncidence physicalMomentum
 237  o2_debit_axis_cauchy : AdditiveOnDebitAxis physicalMomentum
 238  reads_net : ReadsNetImbalance physicalMomentum
 239  swap_odd : SwapOdd physicalMomentum
 240  continuous : Continuous physicalMomentum
 241  unit : physicalMomentum ((1, 0) : LedgerState) ^ 2 = 1
 242  end_to_end_energy_equals_cost :
 243    (∀ z w : LedgerState,
 244      physicalMomentum (z + w) =
 245        physicalMomentum z + physicalMomentum w) ∧
 246      (∀ z : LedgerState, Balanced z → physicalMomentum z = 0) ∧
 247      EnergyEqualsCost physicalMomentum
 248  selection_among_incident :
 249    PostingIncidence physicalMomentum ∧
 250      AdditiveOnDebitAxis physicalMomentum ∧
 251      PostingIncidence cubeDiff ∧
 252      ¬ AdditiveOnDebitAxis cubeDiff ∧
 253      cubeDiff ≠ physicalMomentum
 254
 255theorem physicalMomentumVerdict : PhysicalMomentumVerdict where
 256  definition_eq_imbalance := physicalMomentum_eq_imbalance
 257  o1_posting_incidence := physicalMomentum_posting_incidence
 258  o2_debit_axis_cauchy := physicalMomentum_additiveOnDebitAxis
 259  reads_net := physicalMomentum_readsNetImbalance
 260  swap_odd := physicalMomentum_swap_odd
 261  continuous := physicalMomentum_continuous
 262  unit := physicalMomentum_unit
 263  end_to_end_energy_equals_cost := energyEqualsCost_of_physicalMomentum
 264  selection_among_incident := net_charge_selected_among_incident
 265
 266/-! ## Axiom audit -/
 267
 268#print axioms physicalMomentum_eq_imbalance
 269#print axioms physicalMomentum_posting_incidence
 270#print axioms physicalMomentum_additiveOnDebitAxis
 271#print axioms physicalMomentum_readsNetImbalance
 272#print axioms physicalMomentum_swap_odd
 273#print axioms physicalMomentum_continuous
 274#print axioms physicalMomentum_unit
 275#print axioms physicalMomentum_additive
 276#print axioms energyEqualsCost_of_physicalMomentum
 277#print axioms physicalMomentum_inhabits_posting_package
 278#print axioms cubeDiff_is_not_physicalMomentum
 279#print axioms net_charge_selected_among_incident
 280#print axioms physicalMomentumVerdict
 281
 282end
 283end PhysicalMomentum
 284end SevenGaps
 285end Gravity
 286end IndisputableMonolith
 287