Encyclopedia Masses Masses Mass Genesis T10 Organ Arrow Reduction Intended Gap One Factor Amplitude

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Organ Arrow Reduction Intended Gap One Factor Amplitude

A machine-checked proof pins the intended carrier amplitude above sixteen, narrowing a search that remains open for one class of candidates.

Verify this page

The target amplitude

The declaration intendedGapOneFactorAmplitude_gt_sixteen is a proved theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that a specific real number, called the intended gap-one factor amplitude, is greater than sixteen. This number is not arbitrary: it is defined by the equation f² = φ⁴² / 8, where φ is the golden ratio. The proof uses the fact that φ is at least 3/2, which forces φ⁴² to be greater than 2048, and therefore f² is greater than 256, so f itself is greater than 16.

This single inequality is the capstone of a reduction. The framework's terminal open question asks for an organ arrow, a map that extracts a real number from the settled octave, a discrete record of eight recognition events. The reduction proves that any such map meeting a four-witness interface must name exactly this amplitude f at its octave of use, and must never name its multiples 2f, φf, or φ⁻¹f anywhere else. The inequality then rules out a whole family of simple candidates: the constants 1, 2, and 16 all fall below the target, so none can serve as the organ. The audit extends to the other run-derived constants in the library, including the per-post recognition cost cosh 1 − 1 and the holonomy √2 with its normalizations, and proves each one misses the target.

What the theorem does not claim is just as important. It does not construct the organ arrow; it only reduces the search to naming f from witness data. It proves no impossibility for octave-varying organs, which could return f at one octave and something else elsewhere. The audit is finite, covering only the run-derived reals currently in the library, and is not a classification of all possible quantities. One run-varying family, the posting-count-scaled cost K·(cosh 1 − 1), is closed by later modules using the algebraic/transcendental split: f is algebraic while cosh 1 − 1 is transcendental, so no integer multiple can equal f. The open item remains exactly this: whether any run-derived quantity with independent ancestry can name f.

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 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 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 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 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 proved for octave-varying organs that return f only at one octave. The finite audit is not a classification of all possible run-derived quantities.

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