Encyclopedia Holography Holography Seam Ledger Discharge Ledger Closure Pricing Turn Ratio Cost

ARTICLE 5 claims 5 theorems

Holography Seam Ledger Discharge Ledger Closure Pricing Turn Ratio Cost

A machine-checked proof shows that if a holographic seam's closure cost is read from a 2x2 transfer matrix, the deficit-free period is uniquely forced, no matter how the trace is interpreted.

Verify this page

The discharge theorem

In the Recognition Science framework, a holographic seam (a boundary between two regions of a ledger) carries a closure cost: the price of reconciling the mismatch across that boundary. The framework asks a narrow question: if that cost is computed from a 2x2 matrix that preserves a certain pairing form, does the period of zero cost, called the deficit-free period, have a unique value? The theorem ledgerClosurePricing_turnRatioCost answers yes, and it does so in a deliberately weak way.

The proof works from a ledger (a discrete record of events) and a recognition (a matching of entries). The cost function C(κ, T) takes a rate κ and a period T. The theorem shows that this cost satisfies a condition called LedgerClosurePricing: for any positive κ and T, there exists a 2x2 matrix W that preserves the pairing form, has a real eigenvalue equal to the turn ratio κT, and whose trace, fed through a reading function, gives the cost. The key lemma is that any such conserving matrix has trace at least 2, with equality exactly when the eigenvalue is 1. This trace bound, combined with a calibration condition (trace 2 reads as zero cost) and a faithfulness condition (trace above 2 reads as nonzero cost), forces the cost to vanish if and only if T = 2π/κ.

The theorem's strength is its generality. The reading function, which maps the trace to a cost, is not fixed to a specific form. The result holds for any reading that is calibrated and faithful. This means the deficit-free period is not an artifact of a particular cost formula; it is forced by the ledger structure alone. The theorem also provides a concrete witness: the turnRatioCost function itself satisfies the premises, so the condition is not vacuous. A companion theorem shows that every reading is realized by some induced cost, so the framework is not picking a single special case.

In Recognition Science, this result is called a discharge: it pushes a previously assumed condition down to a weaker, more honest premise. The exact anomaly reading, which gives the cost as J(turnRatio) = (x + 1/x)/2 - 1, is shown to be one valid reading among many for the purpose of locating the zero. The theorem does not claim that the physical seam cost functional actually satisfies LedgerClosurePricing. That instantiation, tying the abstract ledger to a physical system, remains open. The theorem also does not identify the rate κ with a horizon's clock rate; that identification is a separate, unproven step. What the theorem establishes is a conditional: if the ledger closure pricing holds for some calibrated, faithful reading, then the deficit-free period is uniquely 2π/κ.

The practical consequence is that the framework's prediction of a deficit-free period does not depend on the fine details of how cost is read from the trace. A whole family of readings all yield the same zero. This robustness is what the theorem contributes: it separates the structural forcing from the interpretive choice, and shows that the structural part alone is enough to fix the period.

THEOREM ledgerClosurePricing_turnRatioCost · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
ledgerClosurePricing_turnRatioCost · IndisputableMonolith/Holography/SeamLedgerDischarge.lean:287 
/-- **Non-vacuity (THEOREM).** The turn-ratio cost satisfies the weak premise at
the anomaly reading, witnessed by the `hyperbolicWitness` family (CITED, witness
only — never the construction, per the circularity fence). -/
theorem ledgerClosurePricing_turnRatioCost :
    LedgerClosurePricing anomalyReading TurnRatioCarrier.turnRatioCost := 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)
  refine ⟨hyperbolicWitness (turnRatio kappa T),
    (preserves_pairForm_iff_det_one _).mpr hdet,
    hyperbolicWitness_eigen _, ?_⟩
  have hJ : SeamTransferCore.charAnomaly (hyperbolicWitness (turnRatio kappa T))
      = Cost.Jcost (turnRatio kappa T) :=
    charAnomaly_eq_J hdet hx (hyperbolicWitness_eigen _)
  calc TurnRatioCarrier.turnRatioCost kappa T
      = Cost.Jcost (turnRatio kappa T) := rfl
    _ = SeamTransferCore.charAnomaly (hyperbolicWitness (turnRatio kappa T)) :=
        hJ.symm
    _ = anomalyReading.f (hyperbolicWitness (turnRatio kappa T)).trace := rfl
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 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 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 faithfulness_is_load_bearing · calibration_is_load_bearing · IndisputableMonolith/Holography/SeamLedgerDischarge.lean
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
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⟩

What this page does not claim

The physical seam cost functional is proven to satisfy LedgerClosurePricing. The rate κ is identified with a horizon's clock rate. The anomaly reading is the only reading that produces the deficit-free period.

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