Holography Turn Ratio Carrier U1 Extension Zero Set Not Forced

The Choice Behind the Cost

The Recognition Science framework's central cost function, J(x) = (x + 1/x)/2 - 1, is proved as a theorem on the positive real numbers. The declaration u1_extension_zero_set_not_forced addresses a subtle question: what happens if one tries to extend this cost function to the complex numbers, specifically to the unit circle of phases? The answer, proved in the framework's machine-checked library, is that the extension is not unique. Two different extensions, Jprime and Jsecond, both agree with the original J on all positive reals, yet they give different values at the imaginary unit i. One of these extensions, Jsecond, even assigns a cost of zero to i, a point that is not equal to 1. This shows that the zero set of any extension is not forced by the original function's behavior on the reals.

This result is a deliberate dead end. It kills a specific route toward deriving a physical quantity, the Bekenstein bound, by showing that any attempt to apply the J formula directly to a U(1) phase is underdetermined. The framework's own phaseCost function, which applies J verbatim to a complex phase, is proved to be never positive and to vanish on every multiple of 2π, making it useless for singling out a preferred period. The declaration u1_extension_zero_set_not_forced is the kernel record that the choice of how to extend J off the reals is a choice, not a forced object. It does not claim that no extension exists, nor does it claim that all extensions are equally valid for physics. It only establishes the logical fact of underdetermination.

The consequence is a sharpening of the framework's own claims. The cost function's uniqueness theorem applies only to the positive reals, where the turn ratio lives. The framework's B2 result, which derives a unique zero-cost period, relies on this real-valued cost, not on any complex extension. The u1_extension_zero_set_not_forced theorem therefore acts as a guardrail, preventing a misreading of the framework's own results. It clarifies that the framework's power comes from the real turn ratio, not from an imagined extension to complex phases.

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

theorem Jsecond_I : Jsecond Complex.I = 0 := by
  unfold Jsecond
  simp [Complex.I_re]

/-- **Kernel record: the zero set of an agreeing extension is not forced.** `Jsecond`
agrees with `J` on `ℝ₊` yet vanishes at `I ≠ 1`: imposing "zero iff closure" on an
extension ASSUMES B2's conclusion rather than deriving it. -/
theorem u1_extension_zero_set_not_forced :
    ∃ J' : ℂ → ℝ,
      (∀ x : ℝ, 0 < x → J' (x : ℂ) = Cost.Jcost x) ∧
      J' Complex.I = 0 ∧ (Complex.I : ℂ) ≠ 1 := by
  refine ⟨Jsecond, fun x hx => Jsecond_agrees x hx, Jsecond_I, ?_⟩
  intro h
  have := congrArg Complex.im h
  simp at this

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

/-- **Poison lemma (lattice blindness):** the phase-branch cost vanishes on EVERY
`n`-sheeted cover, so it can never single out `n = 1`. Contrast
`turnRatioCost_cover_pos`. -/
theorem phaseCost_vanishes_on_covers (n : ℤ) : phaseCost ((n : ℝ) * (2 * Real.pi)) = 0 := by
  rw [phaseCost_eq, Real.cos_int_mul_two_pi]
  ring

What this page does not claim

This answer does not claim that no extension of J to the complex numbers exists. This answer does not claim that the framework's cost function is invalid or incomplete because its complex extension is not unique. This answer does not claim that the u1_extension_zero_set_not_forced theorem proves anything about the physical value of the Bekenstein bound.

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: