Holography Turn Ratio Carrier Turn Ratio Cost Census Pricing

The Pricing Premise

In the Recognition Science framework, the cost of a repeated cycle is not assumed to be arbitrary. The framework's central theorem proves that any cost function meeting five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The declaration turnRatioCost_censusPricing takes the next step. It states that for a cycle that repeats, the per-cycle cost is J of the real turn ratio, the ratio of the cycle's total angle to one full turn of 2π. This is the pricing premise: it connects the abstract cost function to the concrete price of a recurring pattern.

The declaration itself is a simple identity, proved by reflexivity. It defines a property called CensusPricing: for any positive rate κ and positive period T, the cost C(κ, T) equals J(κT / 2π). The theorem turnRatioCost_censusPricing states that the specific function turnRatioCost, which is defined as J of the turn ratio, satisfies this property. This is not a derivation of the pricing rule from deeper principles. It is a definitional choice, a named premise that the framework adopts. The machine-checked library records it as a theorem only in the sense that the property holds for the chosen definition.

The significance lies in what follows from this premise. Given CensusPricing, the framework proves a unique zero-cost period: the cost is zero if and only if the period equals the Euclidean period 2π/κ. It also proves that every integer multiple of that period, except the period itself, carries strictly positive cost. This means the pricing rule, once adopted, forces the cycle to close exactly once per turn, not twice or three times. The premise also rules out an alternative: applying the J formula directly to a phase angle gives a cost that is never positive and vanishes on every multiple turn, so it cannot single out the once-per-turn closure.

What the declaration does not claim is equally important. It does not prove that the pricing rule is the only possible one. The framework explicitly records that extending J from the positive reals to the complex plane is underdetermined: two different extensions agree with J on the reals but differ at the imaginary unit. The pricing premise is therefore a choice, not a forced consequence. The framework also does not claim that the pricing rule has been derived from the more fundamental ledger of recognition events. That derivation remains an open target. Until it is found, any conclusion that uses CensusPricing is conditional on this one named assumption.

/-- The turn-ratio cost itself satisfies the pricing premise (non-vacuity witness). -/
theorem turnRatioCost_censusPricing : CensusPricing turnRatioCost :=
  fun _ _ _ _ => rfl

/-- **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

/-- **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

/-- **Poison lemma (sign death):** the phase-branch cost is NEVER strictly positive,
so it cannot penalize any deficit. The phase branch cannot force the period. -/
theorem phaseCost_nonpos (δ : ℝ) : phaseCost δ ≤ 0 := by
  rw [phaseCost_eq]
  linarith [Real.cos_le_one δ]

/-- **Kernel record: the U(1)/ℂ extension of `J` is underdetermined.** Two extensions
agree with `Cost.Jcost` on all of `ℝ₊` yet disagree at `I`. Any argument that "extends
J to the phase and reads off the period" is choosing its conclusion. -/
theorem u1_extension_not_unique :
    ∃ J₁ J₂ : ℂ → ℝ,
      (∀ x : ℝ, 0 < x → J₁ (x : ℂ) = Cost.Jcost x) ∧
      (∀ x : ℝ, 0 < x → J₂ (x : ℂ) = Cost.Jcost x) ∧
      ∃ z : ℂ, J₁ z ≠ J₂ z := by
  refine ⟨Jprime, Jsecond, fun x _ => Jprime_agrees x, fun x hx => Jsecond_agrees x hx,
    Complex.I, ?_⟩
  rw [Jprime_I, Jsecond_I]
  norm_num

What this page does not claim

The pricing rule is derived from the recognition ledger; it is a named premise. The extension of J to the complex plane is unique; the framework proves it is not. The phase-branch cost is a viable alternative; the framework proves it is not strictly positive. The declaration proves the physical existence of the eight-tick cycle; that is a separate theorem.

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: