Holography Seam Transfer Core B2 Unique Zero Of Conserving

The unique zero

The declaration b2_unique_zero_of_conserving is a theorem in the machine-checked library of the Recognition Science framework. It concerns a seam, a boundary where two regions of a discrete ledger meet, and the recognition cost, the forced price of registering an event at that boundary. The theorem states that for any cost function satisfying a conservation condition, the cost is zero if and only if the period T equals a specific value called the euclidean period of the turn ratio kappa. In plain terms: there is exactly one period at which the seam's cost vanishes, and that period is determined by the geometry of the turn.

The theorem is a consequence of a longer chain of results in the same module. The chain begins with a 2 by 2 matrix that describes how a seam crossing transforms a pair of ledger entries. The conservation condition means this matrix preserves a certain area-like quantity, which pins its determinant to 1. A theorem called balanced_conjugate then shows that if such a matrix has one real eigenvalue x, it must also have the reciprocal eigenvalue x⁻¹. From this, the trace of the matrix is forced to be x + x⁻¹, and the cost, defined as half the trace minus 1, equals the framework's fundamental cost function J(x). The uniqueness of the zero then follows from the properties of J.

This chain is notable because the cost function J appears nowhere in the input assumptions. The inputs are only a determinant condition and one eigenvalue; the reciprocal eigenvalue and the trace are derived, not assumed. The framework's library proves this reduction: if the physical per-cycle cost is the character anomaly of some balanced transfer, then the pricing premise of the TurnRatioCarrier, which names J, is reduced to a checkable structural fact about the seam. The theorem b2_unique_zero_of_conserving is the final step that turns this reduction into a statement about when the cost is zero.

What the theorem does not claim is equally precise. It does not prove that a physical seam actually delivers such a transfer. That the pair fiber is 2-dimensional over the reals, that one closure acts linearly with the delivered leg scaling by the turn ratio, and that double-entry balance is unimodularity, all remain MODEL assumptions, not theorems. The reduction is proved, but the physical bridge from the seam ledger to the matrix algebra is open. The theorem is also conditional on the conservation condition; if that condition fails, the uniqueness statement does not apply.

The practical payoff is a falsifiable signature. The framework's cost function gives J(3)/J(2) = 8/3, which is not equal to 2. If a physical seam ever prices the triple cover at ratio 2, the trace carrier is dead; 8/3 is its signature. This discriminates between the framework's pairing pricing and a simpler linear pricing, and it gives experimenters a specific number to check.

/-- **The full Phase-B chain, stated once (THEOREM):** a pairing-CONSERVING seam
transfer delivering the turn ratio prices the census by J, and the deficit-free
period `β = 2π/κ` is its unique zero. From ledger conservation to the B2 discharge
with no J, no cosh, no determinant, and no diagonal form anywhere in the premise. -/
theorem b2_unique_zero_of_conserving (C : ℝ → ℝ → ℝ)
    (h : ConservingSeamPricing C) (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa :=
  b2_unique_zero_of_seamTransfer C (seamTransferPricing_of_conserving C h) kappa T hk hT

/-- **Balance forces the reciprocal leg (THEOREM, the circularity fence honored).**
If a balanced transfer has real eigenvalue `x ≠ 0`, then `x⁻¹` is ALSO an eigenvalue:
the conjugate column scales by the reciprocal because the eigenvalue product IS the
determinant and double-entry pins the determinant to 1. This is the panel's guardrail
discharged: `diag(x, x⁻¹)` is never posited; the `x⁻¹` is a consequence of balance. -/
theorem balanced_conjugate {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
    (hdet : W.det = 1) (hx : x ≠ 0) (h : HasRealEigen W x) :
    HasRealEigen W x⁻¹ := by
  have htr := balanced_trace hdet hx h
  have hdet0 : (W - x⁻¹ • (1 : Matrix (Fin 2) (Fin 2) ℝ)).det = 0 := by
    rw [det_sub_smul_one, hdet, htr]
    field_simp
    ring
  obtain ⟨v, hv, hker⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr hdet0
  refine ⟨v, hv, ?_⟩
  have := hker
  rw [Matrix.sub_mulVec, Matrix.smul_mulVec, Matrix.one_mulVec,
    sub_eq_zero] at this
  exact this

/-- **The character anomaly of a balanced transfer IS the T5 cost (THEOREM).**
`Tr(W)/2 − 1 = J(x)` for the delivered ratio `x > 0`. J is never mentioned in the
hypotheses; it emerges from Cayley–Hamilton + balance. -/
theorem charAnomaly_eq_J {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
    (hdet : W.det = 1) (hx : 0 < x) (h : HasRealEigen W x) :
    charAnomaly W = Cost.Jcost x := by
  unfold charAnomaly Cost.Jcost
  rw [balanced_trace hdet (ne_of_gt hx) h]

/-- **The trace-carrier signature: `J(3)/J(2) = 8/3` (THEOREM).** -/
theorem cover_cost_ratio_eq : Cost.Jcost 3 / Cost.Jcost 2 = 8 / 3 := by
  rw [Jcost_two, Jcost_three]
  norm_num

What this page does not claim

The theorem does not prove that any physical seam actually delivers a balanced transfer. The theorem does not apply to cost functions that violate the conservation condition. The theorem does not derive the 2-dimensionality of the pair fiber from the seam ledger.

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/SeamTransferCore.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: