Masses Mass Genesis T10 Field Current Selector Degeneracy

The selector degeneracy

In the Recognition Science framework, the T10 field-to-current selector degeneracy addresses a specific problem: how to derive a law that converts a field into a current, independently of a known target value. The framework's ledger, a discrete record of events, models emitted photon states with an amplitude `a`. The degeneracy triple, a set of three simultaneous facts, states that in this scaled sourced world, at every amplitude, the channel field vanishes identically (`F = 0` and `A = 0`), the Maxwell current is exactly `a` times the unit-amplitude current, and the derived window is exactly `a` times the unit-amplitude window. This means there is no field-side magnitude for a law to use; the current and window carry the amplitude only as an overall linear factor.

The reduction theorem then shows that any uniquely pinning amplitude predicate, one that holds of at most one positive amplitude, that accepts the intended witness pins exactly that intended amplitude. For the canonical linear shape `a * u = C` with `u ≠ 0`, which covers every current and window magnitude law here, the admission gate's three clauses reduce to pure arithmetic about `C`: it accepts the intended witness iff `C = intended * u`, rejects the doubled copy iff `C ≠ 2 * intended * u`, and uniquely pins when `u ≠ 0`. The entire selector question therefore reduces to one line: is the constant `C` derivable from something other than the topology factor?

The census, measured and dated 2026-07-31, finds exactly two derived absolutes on the emission side. The unit posting, a law pinning `a` in posting units, is walled for charged sigma zero, and the intended gap-one amplitude ≈ 8653.6 is not a posting unit, so such a law fails the acceptance clause. The coherence quantum `E_coh = φ⁻⁵` on the event-pricing layer is walled because the intended witness exceeds every block energy, and the counting bridge is irrational. The channel capacity `φ⁴⁵` is an absolute bound, not a selector: as an inequality it accepts the doubled copy, as an equality it rejects the intended witness.

The typed missing map remains open: an independently derived absolute current magnitude `C`, equivalently a genesis-creation predicate that selects the `J`-ground point of the pattern's scale orbit. The conserved load-to-topology ratio already forces selection to happen at genesis rather than in the flow; `R4` is that selection, adopted as a foundational model law, and on Q3 carriers it is pointwise `loadRecognitionCost = 0`, so its content is assumed, not derived. Until then, every field-to-current selector in this world is either homogeneous (dead by `T10JointScaleHomogeneityNoGo`), circular (its constant is the target), or walled (unit posting, coherence quantum).

/-- The scaled sourced channel's field vanishes at every simplex, at every
amplitude. There is no field-side magnitude for a field-to-current law to
use. -/
theorem postedPhotonChannelScaled_field_zero
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (a : ℝ)
    (s : Simplex (postedPhotonChannelScaled octave phase a).mesh 2) :
    (postedPhotonChannelScaled octave phase a).F s = 0 := rfl

/-- The scaled sourced channel's potential vanishes at every simplex. -/
theorem postedPhotonChannelScaled_potential_zero
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (a : ℝ)
    (s : Simplex (postedPhotonChannelScaled octave phase a).mesh 1) :
    (postedPhotonChannelScaled octave phase a).A s = 0 := rfl

/-- The scaled channel's current at every simplex is exactly the amplitude
times the unit-amplitude current. -/
theorem postedPhotonChannelScaled_current_smul
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (a : ℝ)
    (s : Simplex (postedPhotonChannelScaled octave phase a).mesh 1) :
    (postedPhotonChannelScaled octave phase a).J s =
      a * (postedPhotonChannelScaled octave phase 1).J s := by
  simp only [postedPhotonChannelScaled, postedTickCurrentScaled, one_mul]

/-- The derived window is exactly the amplitude times the unit-amplitude
window. -/
theorem emittedWindow_smul
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (a : ℝ) :
    channelTickCurrentScaled octave phase a =
      fun t => a * channelTickCurrentScaled octave phase 1 t := by
  funext t
  have h0 := congrFun
    (channelTickCurrentScaled_eq_scaledCommit octave phase a) t
  have h1 := congrFun
    (channelTickCurrentScaled_eq_scaledCommit octave phase 1) t
  simp only [scaledCommitSettlementWindow] at h0 h1
  rw [h0, h1]
  simp

/-- **Selector reduction.** A uniquely pinning predicate that accepts the
intended witness pins exactly the intended amplitude: the selector's
inhomogeneity IS the constant it names. Independence from the target is
therefore a question about the provenance of that constant, and only that. -/
theorem selector_pin_eq_of_accepts
    {P : ℝ → Prop} (hP : UniquelyPinning P)
    {intended : ℝ} (hintended : 0 < intended) (hacc : P intended)
    {a : ℝ} (ha : 0 < a) (hPa : P a) :
    a = intended :=
  hP a intended ha hintended hPa hacc

/-- **The gate, reduced to arithmetic.** For a nonzero unit magnitude, the
canonical law uniquely pins; it accepts the intended witness iff `C` is the
intended magnitude, and rejects the doubled copy iff `C` is not twice it. -/
theorem linearLaw_gate_iff
    {u intended : ℝ} (hu : u ≠ 0) (hintended : 0 < intended) (C : ℝ) :
    UniquelyPinning (LinearMagnitudeLaw u C) ∧
    (LinearMagnitudeLaw u C intended ↔ C = intended * u) ∧
    (¬ LinearMagnitudeLaw u C (2 * intended) ↔ C ≠ 2 * intended * u) := by
  refine ⟨?_, ?_, ?_⟩
  · intro a b ha hb hCa hCb
    have h1 : a * u = b * u := hCa.trans hCb.symm
    exact mul_right_cancel₀ hu h1
  · constructor
    · intro h
      exact h.symm
    · intro h
      exact h.symm
  · constructor
    · intro hCe hC2
      exact hCe hC2.symm
    · intro hne hC2
      exact hne hC2.symm

What this page does not claim

This answer does not claim that the constant `C` has been derived from first principles. This answer does not claim that the unit posting or coherence quantum laws are the only possible selectors. This answer does not claim that the framework's library contains a creation operator for the sourced world.

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/MassGenesis/T10FieldCurrentSelectorDegeneracy.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: