Holography Seam Cycle Carrier Deficit Cost Even

The even deficit cost

In mathematics, a function is even when flipping the sign of its input leaves the output unchanged: f(−x) = f(x). The classic example is the cosine function, where cos(−θ) = cos(θ). The declaration deficitCost_even proves that a specific cost function, called the deficit cost, has exactly this property. The deficit cost measures the price of a separation or deficit in a recognition cycle, and the theorem states that the cost of a deficit δ equals the cost of its negative, −δ.

The proof is a direct consequence of the cost's definition. The deficit cost is built from the cosine function, and the theorem follows from the trigonometric identity cos(−θ) = cos(θ). This is not an assumption or a model choice; it is a proved result within the framework's machine-checked library of formal theorems. The declaration is a small but concrete piece of a larger structure: it shows that the symmetry of the cost is inherited from the symmetry of the cosine, not imposed by hand.

In Recognition Science, this evenness is not an isolated curiosity. It is the shadow of a deeper principle called reciprocity, the idea that the cost of a separation is the same whether you measure it forward or backward. The framework's unique cost function J(x) satisfies J(x) = J(1/x), and when expressed on an exponential scale, this becomes an even function. The deficit cost, defined on a circular carrier, inherits this same evenness through the cosine. The theorem thus connects a simple trigonometric identity to a structural symmetry of the framework's foundational cost.

The declaration does not claim that the deficit cost is the only possible cost function, nor that its evenness is a new or independent symmetry. It also does not claim that the physical identification of the seam correlator with the cycle flow's pairing correlator is proved; that identification remains a model premise. The theorem only establishes the evenness of a specific function, given its definition, and nothing more.

/-- The deficit-cost J-form on the U(1) carrier is even: `C(−δ) = C(δ)`. The U(1)
shadow of the same reciprocity. -/
theorem deficitCost_even (δ : ℝ) : deficitCost (-δ) = deficitCost δ := by
  unfold DeficitFreePeriod.deficitCost
  rw [Real.cos_neg]

/-- The deficit-cost J-form on the U(1) carrier is even: `C(−δ) = C(δ)`. The U(1)
shadow of the same reciprocity. -/
theorem deficitCost_even (δ : ℝ) : deficitCost (-δ) = deficitCost δ := by
  unfold DeficitFreePeriod.deficitCost
  rw [Real.cos_neg]

/-- On the exponential ladder the unique recognition cost is EVEN in the log
separation: `J(e^a) = J(e^{−a})`. This is exactly T5 reciprocity `J(x) = J(1/x)`
(`Cost.Jcost_symm`) read at `x = e^a`. Evenness of the seam correlator is the
carrier-level form of this reciprocity, not an independent symmetry. -/
theorem Jcost_exp_even (a : ℝ) :
    Cost.Jcost (Real.exp a) = Cost.Jcost (Real.exp (-a)) := by
  rw [Real.exp_neg]
  exact Cost.Jcost_symm (Real.exp_pos a)

What this page does not claim

The deficit cost is the unique cost function for all recognition processes. The evenness of the deficit cost is a new symmetry independent of reciprocity. The physical identification of the seam correlator with the cycle flow's pairing correlator is proved.

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