Masses Mass Genesis T10 Run Cascade Quadratic Scale Boundary Quadratic Run Patte

The quadratic boundary

In the Recognition Science framework, the mass-genesis program asks how particle masses might arise from a discrete recognition ledger, a record of events. One step in that program tries to couple two different mathematical objects: a cascade pairing, which sums weighted contributions across sectors of a settled octave, and an anchor load, a measure of the settled pattern's energy. The declaration quadraticRunPatternBalance_fails_interface is a proved theorem stating that a broad, natural family of such couplings cannot meet the interface, the four required properties that any viable coupling must satisfy.

The theorem's power comes from how much freedom it allows the candidate. The deposit map, the coefficient assignment, and the target function may all inspect the complete proof-carrying settled octave and return arbitrary values. Despite this maximal order-sensitivity, every balance in this class collapses to an equation on the octave alone, because the amplitude-squared factor cancels. This means the candidate is run-only: it depends only on the octave record, not on the amplitude or other carrier details. The interface requires more, so the candidate fails.

The result is a membership theorem, not a new wall. It places this quadratic family inside a class already excluded by an earlier obstruction, T10RunHistoryScaleCouplingBoundary. What is new is showing that the most natural amplitude-bearing candidates, with deposits, coefficients, and target maximally free, still fall into the run-only class. The proved complement of the two killed classes is larger than any named list: filters keyed to pattern support or topology lie outside both, and amplitude-pinning filters with an octave-varying level already meet all four interface witnesses.

The theorem does not claim that no coupling can work. It does not construct or assume any surviving coupling with an independently derived nonzero reference level. It does not classify the complement. The final section supplies a non-vacuity hardening: a concrete run-only filter, exact-octave equality, accepts the intended carrier and therefore violates the ground-state selection property R4. This proves the obstruction is real, not empty.

/-- Main boundary: no unnormalized same-degree cascade/anchor balance in this
maximally order-sensitive class can meet the four-witness interface. -/
theorem quadraticRunPatternBalance_fails_interface {N : ℕ}
    (deposits : Q3SettledLedgerOctave → List (Fin N))
    (coeff : Q3SettledLedgerOctave → SectorN N → ℝ)
    (target : Q3SettledLedgerOctave → ℝ)
    (octave : Q3SettledLedgerOctave) :
    ¬ RunPatternScaleCouplingInterface
        (QuadraticRunPatternBalance deposits coeff target)
        octave := by
  intro hgate
  exact
    (runPatternScaleCouplingInterface_not_runOnly
      (QuadraticRunPatternBalance deposits coeff target)
      octave
      hgate)
      (quadraticRunPatternBalance_isRunOnly
        deposits coeff target)

/-- The candidate balance is equivalent to an equation on the exact octave
alone. Positivity of the carrier amplitude justifies cancellation. -/
theorem quadraticRunPatternBalance_iff_reduced {N : ℕ}
    (deposits : Q3SettledLedgerOctave → List (Fin N))
    (coeff : Q3SettledLedgerOctave → SectorN N → ℝ)
    (target : Q3SettledLedgerOctave → ℝ)
    (c : EmittedScaledSettledReadoutCarrier) :
    QuadraticRunPatternBalance deposits coeff target c ↔
      reducedOrderedCascadePairing deposits coeff c.octave =
        2 * target c.octave := by
  unfold QuadraticRunPatternBalance
  rw [orderedCascadePairing_factor, carrierAnchorLoad_eq]
  unfold postingEventLoad
  have ha2 : c.amplitude ^ 2 ≠ 0 :=
    pow_ne_zero 2 (ne_of_gt c.amplitude_pos)
  constructor
  · intro h
    apply
      mul_left_cancel₀ ha2
    calc
      c.amplitude ^ 2 *
          reducedOrderedCascadePairing deposits coeff c.octave =
        target c.octave * (2 * c.amplitude ^ 2) := h
      _ = c.amplitude ^ 2 * (2 * target c.octave) := by ring
  · intro h
    rw [h]
    ring

/-- Despite arbitrary order-sensitive run dependence, every balance in this
class is run-only. -/
theorem quadraticRunPatternBalance_isRunOnly {N : ℕ}
    (deposits : Q3SettledLedgerOctave → List (Fin N))
    (coeff : Q3SettledLedgerOctave → SectorN N → ℝ)
    (target : Q3SettledLedgerOctave → ℝ) :
    IsRunOnly
      (QuadraticRunPatternBalance deposits coeff target) := by
  intro c d hcd
  constructor
  · intro hc
    apply
      (quadraticRunPatternBalance_iff_reduced
        deposits coeff target d).2
    have hred :=
      (quadraticRunPatternBalance_iff_reduced
        deposits coeff target c).1 hc
    rw [hcd] at hred
    exact hred
  · intro hd
    apply
      (quadraticRunPatternBalance_iff_reduced
        deposits coeff target c).2
    have hred :=
      (quadraticRunPatternBalance_iff_reduced
        deposits coeff target d).1 hd
    rw [hcd]
    exact hred

/-- Non-vacuous instantiation of the banked run-only obstruction. -/
theorem exactOctaveFilter_violates_r4
    (octave : Q3SettledLedgerOctave) :
    ¬ RecognitionGroundStateSelection
      (CarrierRealized (ExactOctaveFilter octave)) :=
  runOnly_carrierRealized_violates_r4
    (ExactOctaveFilter octave)
    (exactOctaveFilter_isRunOnly octave)
    octave
    (exactOctaveFilter_accepts_intended octave)

What this page does not claim

This theorem does not prove that no scale coupling can exist in the framework. It does not classify all possible couplings that survive the obstruction. It does not construct a surviving coupling with an independently derived reference level.

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