Holography Turn Ratio Carrier B2 Unique Zero Of Census Pricing

The Unique Zero-Cost Period

In the Recognition Science framework, a recognition event is a discrete record of something happening, and the cost of that recognition is a fixed, unavoidable price. The framework's library of machine-checked theorems contains a result about a repeated cycle: it proves that, for a given rate of cycling, there is exactly one period of time that carries zero cost. This period is the one where the cycle completes a single full turn, and its length is forced by the framework's own definition of a deficit-free period. The declaration b2_unique_zero_of_censusPricing states this uniqueness: the cost is zero if and only if the period equals that specific, forced value.

The proof rests on a single, explicit premise called CensusPricing. This premise defines the per-cycle cost as a specific function of the ratio between the cycle's period and its natural full-turn time. The result itself is a formal derivation: given that pricing rule, the uniqueness of the zero-cost period follows logically. The library also proves supporting facts: any other period has strictly positive cost, and any multiple of the zero-cost period (representing multiple turns) also costs more than zero. This means the zero-cost period is not just the shortest one, but the only one.

What the result does not claim is that CensusPricing itself is true. That premise is a definitional choice, not a derived result. The framework explicitly labels it as the one remaining physics assumption in this chain. Until this pricing rule is itself derived from more basic principles, the uniqueness result is conditional on it. The result also does not claim that the cost function can be extended to complex numbers in a unique way; the library shows that multiple extensions exist, and the proof does not depend on any such extension.

The practical consequence is a sharp, testable prediction: in any system that follows this pricing rule, a zero-cost cycle must have exactly one specific period. This is not a vague preference for the shortest cycle; it is a mathematical fact that all other periods, including multiples of the shortest one, are strictly penalized. This uniqueness is what the framework means by a 'deficit-free' period, and it is the foundation for its claims about the structure of recognition cycles.

/-- **B2, carrier-agnostic, discharged from the named premise.** ANY per-cycle cost
functional satisfying `CensusPricing` has the deficit-free period `2π/κ` as its UNIQUE
zero: deficits, excesses, and every `n ≥ 2` cover all cost strictly positive
recognition, and the cost accumulates without bound (`accumulatedCost_unbounded`).
FORCED-CONDITIONAL: the tag is set by the `CensusPricing` premise. -/
theorem b2_unique_zero_of_censusPricing (C : ℝ → ℝ → ℝ) (hC : CensusPricing C)
    (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa := by
  rw [hC kappa T hk hT]
  exact turnRatioCost_eq_zero_iff kappa T hk hT

/-- Strict positivity off the deficit-free period: any other positive period, deficit
or excess, costs strictly positive recognition per cycle. -/
theorem turnRatioCost_pos_of_ne_period (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T)
    (hne : T ≠ DeficitFreePeriod.euclideanPeriod kappa) :
    0 < turnRatioCost kappa T := by
  rcases lt_or_eq_of_le (turnRatioCost_nonneg hk hT) with hpos | heq
  · exact hpos
  · exact absurd ((turnRatioCost_eq_zero_iff kappa T hk hT).mp heq.symm) hne

/-- **KMS-window discharge, positivity half:** every `n ≥ 2` sheeted cover (Euclidean
angle `2πn`) carries strictly positive per-cycle cost. The excess-angle branch is
cost-excluded by the same T5 inequality as the deficit branch. -/
theorem turnRatioCost_cover_pos (kappa : ℝ) (hk : 0 < kappa) (n : ℕ) (hn : 2 ≤ n) :
    0 < turnRatioCost kappa (n * DeficitFreePeriod.euclideanPeriod kappa) := by
  unfold turnRatioCost
  rw [turnRatio_cover kappa hk n]
  have hpos : (0 : ℝ) < n := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_two hn
  have hne : (n : ℝ) ≠ 1 := by
    have : (1 : ℝ) < n := by exact_mod_cast Nat.lt_of_lt_of_le Nat.one_lt_two hn
    exact ne_of_gt this
  exact Cost.Jcost_pos_of_ne_one _ hpos hne

/-- **The one remaining physics premise (`CensusPricing` /
`CensusClosureNormalization`), NAMED and TYPED.** The fixed-point per-cycle
recognition cost of the continued cycle at rate `κ` and Euclidean period `T` is `J` of
the turn ratio (the delivered/required closure fraction), posted once per closure.
Under-posting half: `EightTickSubperiodExclusion` (proper sub-periods destroy the
census). Over-posting half: `eight_tick_multiple_exclusion` (covers double-post).
STATUS: MODEL until derived from the seam ledger; consumers of the discharge below are
FORCED-CONDITIONAL on it. -/
def CensusPricing (C : ℝ → ℝ → ℝ) : Prop :=
  ∀ kappa T : ℝ, 0 < kappa → 0 < T → C kappa T = Cost.Jcost (turnRatio kappa T)

What this page does not claim

The result does not prove that the CensusPricing premise is true. The result does not claim that the cost function has a unique extension to complex numbers. The result does not describe a specific physical system that realizes this pricing rule.

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