Encyclopedia Holography Holography Seam Ledger Discharge Ledger Closure Pricing Reading Cost

ARTICLE 5 claims 5 theorems

Holography Seam Ledger Discharge Ledger Closure Pricing Reading Cost

A machine-checked theorem shows that any ledger of recognition events can price its own closure, provided the pricing rule meets two plain conditions.

Verify this page

The reading cost

A ledger is a discrete record of events. In Recognition Science, the framework that derives physics from such records, a seam is the boundary between two adjacent regions of a ledger, and its closure is the act of reconciling what entered and left across that boundary. The declaration ledgerClosurePricing_readingCost establishes that for any way of reading a seam's imbalance, there exists a pricing rule that assigns a cost to that closure, and this rule is consistent with the ledger's own conservation law.

The theorem is one of several in the machine-checked library of formal theorems that together form a certificate for what the framework calls SeamLedgerDischarge. The certificate proves a chain of results. First, any transfer that conserves the ledger's pairing form has a trace equal to x + x⁻¹ for some positive real x, and this trace is always at least 2, with equality exactly when x equals 1. Second, for any reading function that is calibrated (it assigns zero cost to the identity closure, where there is no mismatch) and faithful (it assigns nonzero cost to any strictly imbalanced closure), the pricing rule forces the cost to be zero exactly at one special period, the deficit-free period β = 2π/κ. Third, the theorem named in the question shows that every reading is realized by its own induced cost function, so the framework's pricing scheme is not empty: there is always at least one cost that obeys the rules.

The classical mathematics here is the arithmetic mean of a positive number and its reciprocal. The trace bound x + x⁻¹ ≥ 2 is the AM–GM inequality, with equality only at x = 1. The theorem two_le_add_inv proves this directly. The special reading that the framework calls the anomaly reading, defined by f(t) = t/2 − 1, is equivalent to the older notion of ConservingSeamPricing. At this reading, the cost function is forced to equal the framework's central cost function J(x) = (x + 1/x)/2 − 1, and the unique zero of the per-cycle cost lands at the deficit-free period.

What the declaration does not claim is equally important. It does not claim that any particular physical seam actually satisfies the ledger closure pricing premise. That identification, that the real world's seam cost functional realizes the abstract ledger structure, is explicitly tagged as MODEL-until-derived, an open target. The theorem is conditional: if a seam obeys the ledger closure pricing rules, then the conclusions follow. Whether any physical seam does obey them is a separate, unresolved question. The theorem also does not claim that the anomaly reading is the only possible reading; it shows that every reading in the defined class works, and that dropping either calibration or faithfulness destroys the result.

The practical upshot is a precise boundary on what the framework has established. The formal library proves that a ledger's closure can be priced consistently, and that the pricing rule is tightly constrained by two plain conditions. It does not yet prove that the universe's actual seams implement this scheme. That step, the physical instantiation, remains open, and the framework's own documentation says so plainly.

THEOREM ledgerClosurePricing_readingCost · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
ledgerClosurePricing_readingCost · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:308 
/-- **Non-vacuity for EVERY reading (THEOREM).** Each `TraceReading` is realized by
its own induced cost `R.f (x + x⁻¹)` via the hyperbolic witness family: the weak
premise is inhabited at every admissible reading, so its generality is not vacuous. -/
theorem ledgerClosurePricing_readingCost (R : TraceReading) :
    LedgerClosurePricing R
      (fun kappa T => R.f (turnRatio kappa T + (turnRatio kappa T)⁻¹)) := by
  intro kappa T hk hT
  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
  have hdet : (hyperbolicWitness (turnRatio kappa T)).det = 1 :=
    hyperbolicWitness_det _ (ne_of_gt hx)
  have hcons : ∀ u v, pairForm ((hyperbolicWitness (turnRatio kappa T)).mulVec u)
      ((hyperbolicWitness (turnRatio kappa T)).mulVec v) = pairForm u v :=
    (preserves_pairForm_iff_det_one _).mpr hdet
  refine ⟨hyperbolicWitness (turnRatio kappa T), hcons,
    hyperbolicWitness_eigen _, ?_⟩
  have htr := conserving_trace_eq hcons hx (hyperbolicWitness_eigen _)
  exact congrArg R.f htr.symm
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_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
THEOREM cost_eq_J_of_anomalyLedger · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
cost_eq_J_of_anomalyLedger · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:266 
/-- **The cost is J of the turn ratio (THEOREM, FORCED-CONDITIONAL).** At the
anomaly reading, the weak premise forces `C κ T = J(κT/2π)` — the full T5 pricing,
recovered by citation of the landed chain. -/
theorem cost_eq_J_of_anomalyLedger (C : ℝ → ℝ → ℝ)
    (h : LedgerClosurePricing anomalyReading C)
    (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
    C kappa T = Cost.Jcost (turnRatio kappa T) :=
  censusPricing_of_anomalyLedger C h kappa T hk hT
THEOREM calibration_is_load_bearing · faithfulness_is_load_bearing · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
calibration_is_load_bearing · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:356 
/-- **Calibration is load-bearing (THEOREM).** Dropping `calibrated` (keeping the
faithful reading `f ≡ 1`) admits the constant cost `1`, which has NO zero at all:
the deficit-free period would not be a zero, and B2's existence half fails. -/
theorem calibration_is_load_bearing :
    ∃ C : ℝ → ℝ → ℝ,
      (∀ kappa T : ℝ, 0 < kappa → 0 < T →
        ∃ W : Matrix (Fin 2) (Fin 2) ℝ,
          (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ∧
          HasRealEigen W (turnRatio kappa T) ∧
          C kappa T = (fun _ : ℝ => (1 : ℝ)) W.trace) ∧
      ∀ kappa T : ℝ, C kappa T ≠ 0 := by
  refine ⟨fun _ _ => 1, ?_, fun _ _ => one_ne_zero⟩
  intro kappa T hk hT
  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
  exact ⟨hyperbolicWitness (turnRatio kappa T),
    (preserves_pairForm_iff_det_one _).mpr
      (hyperbolicWitness_det _ (ne_of_gt hx)),
    hyperbolicWitness_eigen _, rfl⟩
faithfulness_is_load_bearing · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:328 
/-- **Faithfulness is load-bearing (THEOREM).** Dropping `faithful` (keeping the
calibrated reading `f ≡ 0`) admits the identically-zero cost, whose zero set
contains periods OFF the deficit-free period: B2's uniqueness fails. So the
faithfulness clause of `TraceReading` is necessary, not decorative. -/
theorem faithfulness_is_load_bearing :
    ∃ C : ℝ → ℝ → ℝ,
      (∀ kappa T : ℝ, 0 < kappa → 0 < T →
        ∃ W : Matrix (Fin 2) (Fin 2) ℝ,
          (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ∧
          HasRealEigen W (turnRatio kappa T) ∧
          C kappa T = (fun _ : ℝ => (0 : ℝ)) W.trace) ∧
      ∃ kappa T : ℝ, 0 < kappa ∧ 0 < T ∧ C kappa T = 0 ∧
        T ≠ DeficitFreePeriod.euclideanPeriod kappa := by
  refine ⟨fun _ _ => 0, ?_, 1, 1, one_pos, one_pos, rfl, ?_⟩
  · intro kappa T hk hT
    have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
    exact ⟨hyperbolicWitness (turnRatio kappa T),
      (preserves_pairForm_iff_det_one _).mpr
        (hyperbolicWitness_det _ (ne_of_gt hx)),
      hyperbolicWitness_eigen _, rfl⟩
  · intro hTeq
    have h1 : turnRatio 1 1 = 1 := (turnRatio_eq_one_iff 1 1 one_pos).mpr hTeq
    have hpi : (3 : ℝ) < Real.pi := Real.pi_gt_three
    have h2pi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
    unfold TurnRatioCarrier.turnRatio at h1
    rw [div_eq_one_iff_eq h2pi] at h1
    linarith

What this page does not claim

The physical seam cost functional satisfies the ledger closure pricing premise. The anomaly reading is the only possible reading. The theorem proves anything about the physical world without the conditional premise being satisfied.

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