Encyclopedia Masses Masses Channel Cost Boundary Channel Cost Shift Rational Pos Iff

ARTICLE 3 claims 3 theorems

Masses Channel Cost Boundary Channel Cost Shift Rational Pos Iff

A theorem in the Recognition Science library classifies exactly when a deformed mass-channel cost is a positive rational number, and it does not claim that any particular deformation is the real one.

Verify this page

The shift theorem

The declaration channel_cost_shift_rational_pos_iff is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns the golden ratio φ and a function J that the framework uses to price recognition events. The statement is about a family of costs obtained by shifting a base coefficient by k rungs per channel. The theorem says, for any integer k, that the shifted cost J(φ^(2+k)) is a positive rational number if and only if k is even and k is not equal to -2.

This is a precise classification. For example, when k = 0, the cost is J(φ²) = 1/2, a positive rational. When k = 2, the cost is J(φ⁴) = 5/2, also rational. When k = 1, the cost involves √5 and is irrational. The excluded case k = -2 gives J(φ⁰) = J(1) = 0, which is rational but not positive. The theorem also proves a minimality property: among all positive rational costs in this family, the smallest is 1/2, attained only at k = 0 and its mirror k = -4, a consequence of the symmetry J(x) = J(x⁻¹).

In the framework's account, this theorem does not establish that any particular shift is the correct description of nature. The library proves the classification and the minimality, but it does not prove that a channel's cost must be a positive rational on this ladder, nor that an elementary coupling pays the minimal cost. Those are premises. The theorem sharpens the missing premise from an exact number to a qualitative selection principle: if a channel cost is a positive rational on the golden ladder, minimal among such, and directed upward, then the shift is k = 0. The proof of that conditional is banked as rational_minimal_channel_cost_closes_base, but the antecedent remains open.

THEOREM channel_cost_shift_rational_pos_iff · IndisputableMonolith/Masses/ChannelCostBoundary.lean
channel_cost_shift_rational_pos_iff · IndisputableMonolith/Masses/ChannelCostBoundary.lean:331 
/-- **THEOREM (the rational positive shifts are exactly the even nonzero ones).** The
    deformed per-channel cost `J(φ^{2+k})` is a positive rational iff `k` is even and
    `k ≠ -2`. So requiring a rational channel cost halves the deformation family to the even
    shifts (the odd shifts are irrational; `k = -2` is the zero-cost `φ⁰`). -/
theorem channel_cost_shift_rational_pos_iff (k : ℤ) :
    ((∃ q : ℚ, Cost.Jcost (phi ^ (2 + k)) = (q : ℝ)) ∧ 0 < Cost.Jcost (phi ^ (2 + k)))
      ↔ (Even k ∧ k ≠ -2) := by
  rw [jcost_phi_zpow_natAbs]
  set n := (2 + k).natAbs with hn
  have hrat : (∃ q : ℚ, Cost.Jcost (phi ^ (n : ℕ)) = (q : ℝ)) ↔ n = 0 ∨ Even n :=
    jcost_phi_pow_rational_iff n
  have hpos : 0 < Cost.Jcost (phi ^ (n : ℕ)) ↔ n ≠ 0 := by
    constructor
    · intro hp h0
      rw [h0, pow_zero, Cost.Jcost_unit0] at hp
      exact lt_irrefl _ hp
    · intro h0
      have hn1 : 1 ≤ n := by omega
      have h1 : (1 : ℝ) < phi ^ n := by
        have := pow_lt_pow_right₀ Constants.one_lt_phi hn1
        rwa [pow_zero] at this
      have hlt := Foundation.jcost_strictMono_one_lt (le_refl (1 : ℝ)) h1
      rwa [Cost.Jcost_unit0] at hlt
  rw [hrat, hpos]
  constructor
  · rintro ⟨(h0 | hE), hne⟩
    · omega
    · have hE' : Even (2 + k) := (even_natAbs_iff (2 + k)).1 hE
      have hk2 : k ≠ -2 := by
        intro hk2
        apply hne
        rw [hn, hk2]
        decide
      rcases hE' with ⟨a, ha⟩
      exact ⟨⟨a - 1, by omega⟩, hk2⟩
  · rintro ⟨hEk, hk2⟩
    have hE' : Even (2 + k) := by
      rcases hEk with ⟨a, ha⟩
      exact ⟨a + 1, by omega⟩
    have hnE : Even n := (even_natAbs_iff (2 + k)).2 hE'
    have hn0 : n ≠ 0 := by
      intro h0
      rw [hn, Int.natAbs_eq_zero] at h0
      omega
    exact ⟨Or.inr hnE, hn0⟩
THEOREM channel_cost_shift_minimal · IndisputableMonolith/Masses/ChannelCostBoundary.lean
channel_cost_shift_minimal · IndisputableMonolith/Masses/ChannelCostBoundary.lean:377 
/-- **THEOREM (the canonical shift and its mirror are the unique minima).** Among shifts
    with positive rational channel cost, the cost is at least `1/2`, with equality iff
    `k = 0` (the canonical table) or `k = -4` (the mirror: `φ^{-2}` costs the same as `φ²`
    by `J(x) = J(x⁻¹)`). The upward, mass-lifting choice is `k = 0` alone. -/
theorem channel_cost_shift_minimal (k : ℤ)
    (hrat : ∃ q : ℚ, Cost.Jcost (phi ^ (2 + k)) = (q : ℝ))
    (hpos : 0 < Cost.Jcost (phi ^ (2 + k))) :
    1 / 2 ≤ Cost.Jcost (phi ^ (2 + k))
      ∧ (Cost.Jcost (phi ^ (2 + k)) = 1 / 2 → k = 0 ∨ k = -4) := by
  rw [jcost_phi_zpow_natAbs] at hrat hpos ⊢
  set n := (2 + k).natAbs with hn
  have hn1 : 1 ≤ n := by
    by_contra h0
    push_neg at h0
    have hz : n = 0 := by omega
    rw [hz, pow_zero, Cost.Jcost_unit0] at hpos
    exact lt_irrefl _ hpos
  have hmin := jcost_phi_sq_minimal n hn1 hrat
  refine ⟨hmin.1, fun heq => ?_⟩
  have hn2 : n = 2 := hmin.2 heq
  rw [hn] at hn2
  have h2 : (2 + k).natAbs = ((2 : ℤ)).natAbs := hn2
  rw [Int.natAbs_eq_natAbs_iff] at h2
  rcases h2 with h | h <;> omega
THEOREM channel_cost_boundary · IndisputableMonolith/Masses/ChannelCostBoundary.lean
channel_cost_boundary · IndisputableMonolith/Masses/ChannelCostBoundary.lean:404 
/-- **THEOREM (channel cost is kernel-contingent, stratified).** One conjunction:

    1. every integer per-channel shift meets the table's entire banked structure (torsion
       factorization, channel linearity, the ν3 anomaly);
    2. nonzero shifts are observably distinct — the cost is contingent, not gauge;
    3. the shifts keeping the cost a positive rational are exactly the even nonzero ones;
    4. among those, the minimum `1/2` is attained exactly at the canonical `k = 0` and its
       cost mirror `k = -4`;
    5. conditional closure: a per-channel rung count that is positive, rational, and minimal
       among such is forced to be `2`, which closes the base rule.

    So the kernel does not price a gauge channel; but the price, *if* it is a minimal
    positive rational golden cost directed upward, is forced to be the `φ²`-step. -/
theorem channel_cost_boundary :
    (∀ k : ℤ, ∀ f : Fermion,
      shiftedRungs k f
        = (2 + k) * activeChannelClasses f + Integers.tau (genOf f).val
          + (if f = Fermion.nu3 then 2 else 0))
    ∧ (∀ k : ℤ, k ≠ 0 → ∀ Z : ℤ,
        predictAt .Lepton (deformedTotal k Fermion.e) Z
          ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z)
    ∧ (∀ k : ℤ,
        ((∃ q : ℚ, Cost.Jcost (phi ^ (2 + k)) = (q : ℝ))
            ∧ 0 < Cost.Jcost (phi ^ (2 + k)))
          ↔ (Even k ∧ k ≠ -2))
    ∧ (∀ k : ℤ,
        (∃ q : ℚ, Cost.Jcost (phi ^ (2 + k)) = (q : ℝ)) →
        0 < Cost.Jcost (phi ^ (2 + k)) →
        1 / 2 ≤ Cost.Jcost (phi ^ (2 + k))
          ∧ (Cost.Jcost (phi ^ (2 + k)) = 1 / 2 → k = 0 ∨ k = -4))
    ∧ (∀ k : ℕ, 1 ≤ k →
        (∃ q : ℚ, Cost.Jcost (phi ^ k) = (q : ℝ)) →
        (∀ m : ℕ, 1 ≤ m → (∃ q : ℚ, Cost.Jcost (phi ^ m) = (q : ℝ)) → k ≤ m) →
        ∀ f : Fermion, (k : ℤ) * activeChannelClasses f = 2 * activeChannelClasses f) :=
  ⟨shiftedRungs_factors,
   fun k hk Z => baseRule_predictions_differ k hk Z,
   channel_cost_shift_rational_pos_iff,
   channel_cost_shift_minimal,
   fun k hk hrat hmin f => rational_minimal_channel_cost_closes_base k hk hrat hmin f⟩

What this page does not claim

This theorem does not claim that any particular shift k is the one realized in nature. This theorem does not claim that the cost of a channel must be rational, only classifies when it is. This theorem does not prove the base rule coefficient 2; it only proves a conditional that would close it given an unproved premise.

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/Masses/ChannelCostBoundary.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND