Encyclopedia Masses Masses Mass Genesis T10 Organ Arrow Reduction Carrier Realized Filter Iff Of Pat

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Organ Arrow Reduction Carrier Realized Filter Iff Of Pat

A machine-checked theorem turns a question about particle-mass patterns into a single condition on a real number, and then checks which numbers can pass.

Verify this page

The organ arrow's test

In the Recognition Science account of particle masses, the framework models a settled octave as a discrete record of events, a ledger with eight phases, and asks whether a pattern of emitted signals can be read back from that record. The declaration carrierRealized_filter_iff_of_pattern is a proved equivalence that answers part of that question. It states: a filter that pins an emitted pattern's amplitude realizes a given pattern if and only if the level function, which names a real number from the extracted data, returns that pattern's amplitude at some octave. Rejection is therefore a global property of the level function, not a property of any single carrier.

An organ arrow is any extraction map from the settled octave to any type, together with a level functional on the extracted data. Its induced carrier filter pins the amplitude: the carrier's amplitude equals the level of the extracted octave. The extraction is quantified over every function of the octave, so the committed event witness, the modular-seed data, the Gray walk, and any future run-derived record are all covered. The theorem's three instantiations apply it to the doubled, phi-scaled, and inverse-phi-scaled patterns, each time reducing realization to a condition on the level's values.

The main interface theorem, organArrow_interface_iff, sharpens this: an organ arrow meets the four-witness interface at an octave if and only if its level equals the intended gap-one factor amplitude at that octave and never equals twice that amplitude, phi times it, or phi inverse times it at any octave. The organ question is exactly: name the intended amplitude from witness data, with global decoy avoidance. A constant organ, one that returns the same number at every octave, meets the interface if and only if that constant is the target itself, which is the shape the admission gate's target-independence clause excludes.

The finite audit then checks which run-derived constants currently in the library can name the target. The intended amplitude is greater than 16, so 1, 2, and 16 miss it. The non-rational constants from the 2026-08-01 tree sweep, the per-post recognition cost cosh 1 minus 1 and the holonomy family sqrt 2, 1/sqrt 2, and sqrt 2/4, all miss it. A run-varying family, the atomic posting recognition cost K times (cosh 1 minus 1), is closed by successor modules: the algebraic/transcendental split proves that no nonzero integer multiple of cosh 1 minus 1 equals the target, which is algebraic, so the entire registered cone is closed against naming it.

What the declaration does not claim is as important as what it proves. No organ is constructed. No impossibility theorem is claimed for octave-varying organs: such an organ must return the target at the octave of use, and whether any run-derived quantity can do that with independent ancestry remains open. The finite audit covers only the run-derived reals presently in the library and is not a classification. The interface is a specification, not a provenance certificate.

THEOREM carrierRealized_filter_iff_of_pattern · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean
carrierRealized_filter_iff_of_pattern · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean:239 
private theorem carrierRealized_filter_iff_of_pattern
    (A : OrganArrow) (ψ : LightPattern (Fin 8)) (hψ : Q3MatterCarrier ψ)
    {v : ℝ} (hv : 0 < v)
    (hwindow : ψ.window 0 = fun t => (v : ℂ) * gapOneTwoPhaseMode t) :
    CarrierRealized A.filter ψ ↔
      ∃ o' : Q3SettledLedgerOctave, A.level (A.W o') = v := by
  constructor
  · rintro ⟨c, hc, hpattern⟩
    have hce : c.amplitude = A.level (A.W c.octave) := hc
    refine ⟨c.octave, ?_⟩
    have hw1 : c.pattern.window 0 =
        fun t => (c.amplitude : ℂ) * gapOneTwoPhaseMode t := by
      have h := c.reads_emitted
      rw [originEmittedScaled_window_eq_scaledGapOne] at h
      exact h
    have hcam : c.amplitude = v := by
      apply amplitude_eq_of_window_eq
      rw [← hw1, ← hwindow, hpattern]
    rw [← hce]
    exact hcam
  · rintro ⟨o', ho'⟩
    exact ⟨carrierAtOctave o' hv ψ hψ hwindow, ho'.symm, rfl⟩
THEOREM organArrow_interface_iff · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean
organArrow_interface_iff · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean:303 
/-- Main reduction: an organ arrow meets the four-witness interface at `o`
iff its level names the target at `o` and never names a decoy scale at any
octave. -/
theorem organArrow_interface_iff (A : OrganArrow) (o : Q3SettledLedgerOctave) :
    RunPatternScaleCouplingInterface A.filter o ↔
      A.level (A.W o) = intendedGapOneFactorAmplitude ∧
        (∀ o' : Q3SettledLedgerOctave,
          A.level (A.W o') ≠ 2 * intendedGapOneFactorAmplitude) ∧
        (∀ o' : Q3SettledLedgerOctave,
          A.level (A.W o') ≠ Constants.phi * intendedGapOneFactorAmplitude) ∧
        (∀ o' : Q3SettledLedgerOctave,
          A.level (A.W o') ≠ Constants.phi⁻¹ * intendedGapOneFactorAmplitude) := by
  unfold RunPatternScaleCouplingInterface
  rw [carrierRealized_filter_doubled_iff, carrierRealized_filter_phiScaled_iff,
    carrierRealized_filter_inversePhiScaled_iff]
  constructor
  · rintro ⟨haccept, hd, hφ, hφinv⟩
    have hce : (intendedGapOneFactorCarrier o).amplitude =
        A.level (A.W (intendedGapOneFactorCarrier o).octave) := haccept
    rw [intendedGapOneFactorCarrier_amplitude,
      intendedGapOneFactorCarrier_octave] at hce
    refine ⟨hce.symm, fun o' h => hd ⟨o', h⟩, fun o' h => hφ ⟨o', h⟩,
      fun o' h => hφinv ⟨o', h⟩⟩
  · rintro ⟨hlevel, hd, hφ, hφinv⟩
    refine ⟨?_, ?_, ?_, ?_⟩
    · have hce : (intendedGapOneFactorCarrier o).amplitude =
          A.level (A.W (intendedGapOneFactorCarrier o).octave) := by
        rw [intendedGapOneFactorCarrier_amplitude,
          intendedGapOneFactorCarrier_octave]
        exact hlevel.symm
      exact hce
    · rintro ⟨o', h⟩
      exact hd o' h
    · rintro ⟨o', h⟩
      exact hφ o' h
    · rintro ⟨o', h⟩
      exact hφinv o' h
THEOREM constantArrow_interface_iff · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean
constantArrow_interface_iff · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean:341 
/-- An octave-invariant organ meets the interface iff it pins exactly the
target: constant organs are precisely target-pinning. -/
theorem constantArrow_interface_iff (K : ℝ) (o : Q3SettledLedgerOctave) :
    RunPatternScaleCouplingInterface (constantArrow K).filter o ↔
      K = intendedGapOneFactorAmplitude := by
  rw [organArrow_interface_iff]
  constructor
  · intro h
    exact h.1
  · intro hK
    have hf := intendedGapOneFactorAmplitude_pos
    have hφ1 : (1 : ℝ) < Constants.phi := Constants.one_lt_phi
    have hφinv1 : Constants.phi⁻¹ < 1 := inv_lt_one_of_one_lt₀ Constants.one_lt_phi
    refine ⟨hK, fun o' => ?_, fun o' => ?_, fun o' => ?_⟩
    · show K ≠ 2 * intendedGapOneFactorAmplitude
      rw [hK]
      intro h
      nlinarith [hf]
    · show K ≠ Constants.phi * intendedGapOneFactorAmplitude
      rw [hK]
      intro h
      nlinarith [hf, hφ1]
    · show K ≠ Constants.phi⁻¹ * intendedGapOneFactorAmplitude
      rw [hK]
      intro h
      nlinarith [hf, hφinv1]
THEOREM intendedGapOneFactorAmplitude_gt_sixteen · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean
intendedGapOneFactorAmplitude_gt_sixteen · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean:400 
/-- The intended amplitude exceeds 16, from `f² = φ⁴²/8 > 256`. -/
theorem intendedGapOneFactorAmplitude_gt_sixteen :
    (16 : ℝ) < intendedGapOneFactorAmplitude := by
  have hsq : intendedGapOneFactorAmplitude ^ 2 = Constants.phi ^ (42 : ℕ) / 8 :=
    gapOne_factorAmplitude_sq_eq_phi42_div_eight
  have h2 : (16 : ℝ) ^ 2 < intendedGapOneFactorAmplitude ^ 2 := by
    rw [hsq]
    linarith [phi42_gt_2048]
  exact lt_of_pow_lt_pow_left₀ 2 (le_of_lt intendedGapOneFactorAmplitude_pos) h2
THEOREM run_derived_reals_audit · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean
run_derived_reals_audit · IndisputableMonolith/Masses/MassGenesis/T10OrganArrowReduction.lean:492 
/-- Finite audit: the unit bridge, the per-phase settlement quantum, the
cycle total, the per-post J-cost, the holonomy √2, and the two deposit
normalizations (`postingNorm = 1/√2`, `creationDepositNorm = √2/4`) are the
run-derived constant reals currently in the library, and all miss the
target. -/
theorem run_derived_reals_audit :
    (1 : ℝ) ≠ intendedGapOneFactorAmplitude ∧
      (2 : ℝ) ≠ intendedGapOneFactorAmplitude ∧
        (16 : ℝ) ≠ intendedGapOneFactorAmplitude ∧
          (Real.cosh 1 - 1 ≠ intendedGapOneFactorAmplitude ∧
            Real.sqrt 2 ≠ intendedGapOneFactorAmplitude) ∧
          (1 / Real.sqrt 2 ≠ intendedGapOneFactorAmplitude ∧
            Real.sqrt 2 / 4 ≠ intendedGapOneFactorAmplitude) ∧
          (∑ phase : Fin 8,
            settlementLoad
              (ledgerOccupationWindow canonicalQ3SettledLedgerOctave phase)) =
            16 :=
  ⟨one_ne_intended, two_ne_intended, sixteen_ne_intended,
    ⟨coshOneSubOne_ne_intended, sqrtTwo_ne_intended⟩,
    ⟨invSqrtTwo_ne_intended, sqrtTwoDivFour_ne_intended⟩,
    canonicalCycleSettlementLoad_eq_sixteen⟩

What this page does not claim

No organ arrow is constructed by this theorem. No impossibility is claimed for octave-varying organs. The finite audit is not a classification of all possible run-derived constants.

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/T10OrganArrowReduction.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