Encyclopedia Holography Holography Seam Ledger Discharge Anomaly Ledger Iff Conserving

ARTICLE 4 claims 4 theorems

Holography Seam Ledger Discharge Anomaly Ledger Iff Conserving

A machine-checked theorem shows that a specific way of reading a ledger's cost is not a special assumption but a restatement of a more basic conservation rule.

Verify this page

The anomaly bridge

In the Recognition Science framework, a ledger is a discrete record of events, and its cost is a number assigned to each possible transition. The declaration anomalyLedger_iff_conserving proves an equivalence. It says that a ledger whose cost is read through the specific formula f(t) = t/2 - 1 is exactly the same as a ledger that obeys a conservation rule for a certain pairing. In plainer terms: choosing that particular reading is not an extra assumption. It is a different way of writing down the same underlying requirement that some quantity is preserved.

The theorem is proved in the machine-checked library of formal theorems, with no unverified axioms. The proof rests on a chain of existing results. A conserving transfer, one that preserves the pairing, must have a trace equal to x + x⁻¹ for its real eigenvalue x. Since x + x⁻¹ ≥ 2 for any positive x, with equality only at x = 1, the trace is always at least 2. The anomaly reading f(t) = t/2 - 1 then maps this trace to a cost, and the equivalence follows by matching the two definitions.

This equivalence matters because it lets the framework transfer a known result. The theorem b2_unique_zero_of_anomalyLedger then shows that, under this reading, the cost is zero exactly when the period T equals 2π/κ, for a positive parameter κ. This period is called the deficit-free period. The result is conditional: it holds for any cost function that satisfies the ledger closure pricing condition with the anomaly reading.

The theorem does not claim that the anomaly reading is the only possible one. The framework also proves that any reading satisfying two plain conditions, calibration and faithfulness, forces the same zero set. Calibration means the identity closure posts zero cost; faithfulness means a strictly imbalanced closure cannot read as free. The anomaly reading is one such reading, and the equivalence shows it is a natural one, but the zero-set result is more general.

The theorem also does not claim that the physical seam cost functional actually satisfies the ledger closure pricing condition. That remains an open question, tagged as a model until derived. The equivalence is a statement about the framework's internal definitions, not a claim about any specific physical system.

THEOREM anomalyLedger_iff_conserving · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
anomalyLedger_iff_conserving · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:243 
/-- **The anomaly instance is exactly the landed premise (THEOREM).** At the
character-anomaly reading, `LedgerClosurePricing` and `ConservingSeamPricing` are
equivalent: the weak premise strictly GENERALIZES the landed one (any other
calibrated faithful reading is also admitted), losing nothing at the anomaly point. -/
theorem anomalyLedger_iff_conserving (C : ℝ → ℝ → ℝ) :
    LedgerClosurePricing anomalyReading C ↔
      SeamTransferCore.ConservingSeamPricing C := by
  constructor
  · exact conservingSeamPricing_of_anomalyLedger C
  · intro h kappa T hk hT
    obtain ⟨W, hcons, heig, hC⟩ := h kappa T hk hT
    exact ⟨W, hcons, heig, hC.trans rfl⟩
THEOREM conserving_trace_bound · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
conserving_trace_bound · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:110 
/-- **The key new lemma, bundled (THEOREM):** for pairing-conserving `W` with real
eigenvalue `x > 0`, `Tr W = x + x⁻¹ ≥ 2`, with equality iff `x = 1`. This is what
lets the discharge below run on ANY calibrated faithful trace reading, not just the
character anomaly: the trace separates "deficit-free" from "mismatched" all by
itself. -/
theorem conserving_trace_bound {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
    (hcons : ∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v)
    (hx : 0 < x) (h : HasRealEigen W x) :
    W.trace = x + x⁻¹ ∧ 2 ≤ W.trace ∧ (W.trace = 2 ↔ x = 1) :=
  ⟨conserving_trace_eq hcons hx h, conserving_trace_ge_two hcons hx h,
    conserving_trace_eq_two_iff hcons hx h⟩
THEOREM b2_unique_zero_of_anomalyLedger · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
b2_unique_zero_of_anomalyLedger · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:275 
/-- **B2 through the landed chain (THEOREM, CITED).** At the anomaly reading the B2
discharge also follows from `b2_unique_zero_of_conserving` — consistency check that
the weak route and the landed route agree on the zero set. -/
theorem b2_unique_zero_of_anomalyLedger (C : ℝ → ℝ → ℝ)
    (h : LedgerClosurePricing anomalyReading C)
    (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa :=
  b2_unique_zero_of_conserving C
    (conservingSeamPricing_of_anomalyLedger C h) kappa T hk hT
THEOREM b2_unique_zero_of_ledgerClosure · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
b2_unique_zero_of_ledgerClosure · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:181 
/-- **B2 from the weak residue (THEOREM, FORCED-CONDITIONAL on
`LedgerClosurePricing`).** For ANY calibrated faithful trace reading, the
deficit-free period `β = 2π/κ` is the UNIQUE zero of the per-cycle cost:

* off the period, `turnRatio ≠ 1` (`turnRatio_eq_one_iff`, CITED), so the trace is
  strictly above 2 (`conserving_trace_bound`) and faithfulness forbids a zero;
* at the period, `turnRatio = 1`, the trace is exactly 2, and calibration fires.

The character anomaly appears NOWHERE: the B2 zero set is forced by conservation,
delivery, calibration, and faithfulness alone. -/
theorem b2_unique_zero_of_ledgerClosure (R : TraceReading) (C : ℝ → ℝ → ℝ)
    (h : LedgerClosurePricing R C) (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa := by
  obtain ⟨W, hcons, heig, hC⟩ := h kappa T hk hT
  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
  rw [hC]
  constructor
  · intro h0
    by_contra hne
    have hx1 : turnRatio kappa T ≠ 1 := fun h1 =>
      hne ((turnRatio_eq_one_iff kappa T hk).mp h1)
    have htr2 : W.trace ≠ 2 := fun heq =>
      hx1 ((conserving_trace_eq_two_iff hcons hx heig).mp heq)
    have hgt : 2 < W.trace :=
      lt_of_le_of_ne (conserving_trace_ge_two hcons hx heig) (Ne.symm htr2)
    exact R.faithful W.trace hgt h0
  · intro hTeq
    have hx1 : turnRatio kappa T = 1 := (turnRatio_eq_one_iff kappa T hk).mpr hTeq
    have htr : W.trace = 2 := by
      rw [conserving_trace_eq hcons hx heig, hx1]
      norm_num
    rw [htr]
    exact R.calibrated

What this page does not claim

The anomaly reading is the only reading that forces the zero set. The physical seam cost functional satisfies the ledger closure pricing condition. The parameter κ is identified with any physical clock rate.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/SeamLedgerDischarge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND