Masses Mass Genesis T10 Channel Block Window Pricing Wall

/-- Every forced channel-block energy is at most one: `phi^(-n) ≤ 1` because
`phi > 1`. Stated against `PostingEventChannelEnergy3.blockEnergy` via
`blockEnergy_forced`, so it is a fact about the pricing law. -/
theorem channelBlockEnergy_le_one
    {N : ℕ} [NeZero N]
    (channelEnergy : PostingEventChannelEnergy3 N)
    (event : RealizedPostingEvent3 N) (n : ℕ) :
    channelEnergy.blockEnergy event n ≤ 1 := by
  rw [channelEnergy.blockEnergy_forced event n]
  have hφ : 1 ≤ phi := phi_ge_one
  have hpow : 1 ≤ phi ^ n := one_le_pow₀ hφ
  calc
    phi ^ (-(n : ℤ)) = (phi ^ n)⁻¹ := by
      rw [zpow_neg, zpow_natCast]
    _ ≤ 1 := inv_le_one_of_one_le₀ hpow

/-- Two-phase window energy of the intended gap-one factor witness. -/
theorem gapOne_factorWindowEnergy_eq_phi42_div_four :
    eightTickWindowEnergy
        (originEmittedPhotonStateScaled
          canonicalQ3SettledLedgerOctave
          (primitivePositiveStationaryFactorAmplitude
            (worldlinePattern gapOneTwoPhaseMode))
          gapOne_factorAmplitude_pos).window =
      phi ^ (42 : ℕ) / 4 := by
  set a :=
    primitivePositiveStationaryFactorAmplitude
      (worldlinePattern gapOneTwoPhaseMode)
  have ha := gapOne_factorAmplitude_pos
  set ψ := scalePattern a (worldlinePattern gapOneTwoPhaseMode)
  have hpack := scalePattern_gapOne_at_factorAmplitude_sigmaZero
  have hwin : SettledAnchorWindow a ψ := hpack.1
  have hread :
      PhotonWindowReadsPatternAnchor
        (originEmittedPhotonStateScaled
          canonicalQ3SettledLedgerOctave a ha).window ψ :=
    factorAmplitude_originEmitted_reads_scaledGapOne
      canonicalQ3SettledLedgerOctave
  have hwindow :
      (originEmittedPhotonStateScaled
          canonicalQ3SettledLedgerOctave a ha).window =
        ψ.window 0 := by
    unfold PhotonWindowReadsPatternAnchor at hread
    exact hread.symm
  have hneut := settledAnchor_neutral hwin
  have hnorm :
      normSq8 (ψ.window 0) = 2 * a ^ 2 := by
    rw [← neutralize_of_neutral (ψ.window 0) hneut]
    exact settledAnchor_neutralizedNormSq hwin
  have hfac := gapOne_factorAmplitude_sq_eq_phi42_div_eight
  unfold eightTickWindowEnergy
  rw [hwindow, hnorm, hfac]
  ring

/-- Honest inequality from `1 < phi`: the intended window energy exceeds one. -/
theorem one_lt_gapOne_factorWindowEnergy :
    (1 : ℝ) < phi ^ (42 : ℕ) / 4 := by
  have hgt : (4 : ℝ) < phi ^ (42 : ℕ) := phi_pow_fortyTwo_gt_four
  have hpos : (0 : ℝ) < 4 := by norm_num
  exact (one_lt_div hpos).2 (by linarith)

/-- No channel-block energy can equal the intended gap-one window energy:
every price is `≤ 1`, while that window is `phi^42/4 > 1`. -/
theorem gapOne_factorWindowEnergy_ne_channelBlockEnergy
    {N : ℕ} [NeZero N]
    (channelEnergy : PostingEventChannelEnergy3 N)
    (event : RealizedPostingEvent3 N) (n : ℕ) :
    eightTickWindowEnergy
        (originEmittedPhotonStateScaled canonicalQ3SettledLedgerOctave
          (primitivePositiveStationaryFactorAmplitude
            (worldlinePattern gapOneTwoPhaseMode))
          gapOne_factorAmplitude_pos).window ≠
      channelEnergy.blockEnergy event n := by
  intro heq
  have hwin := gapOne_factorWindowEnergy_eq_phi42_div_four
  have hle := channelBlockEnergy_le_one channelEnergy event n
  have hgt := one_lt_gapOne_factorWindowEnergy
  linarith

/-- On the neutral Electroweak seed the required weight is `phi^47/4`. -/
theorem electroweak_neutral_requiredEventWeight_eq_phi47_div_four :
    requiredChannelBlockEventWeight Anchor.Sector.Electroweak 0 0 =
      phi ^ (47 : ℕ) / 4 := by
  unfold requiredChannelBlockEventWeight
  rw [Anchor.B_pow_Electroweak_eq, YardstickPremiseFreeCert.r0_ew_certified_eq_55,
    MassLaw.gap_zero_neutral]
  have h2 : (2 : ℝ) ^ ((1 : ℤ) - 3) = (1 : ℝ) / 4 := by
    norm_num
  rw [h2]
  have hexp : ((55 : ℤ) : ℝ) + ((0 : ℤ) : ℝ) - 8 + (0 : ℝ) = (47 : ℝ) := by
    norm_num
  rw [hexp]
  -- `phi ^ (47 : ℝ)` is the real power; reduce to Nat power.
  have h47 : (47 : ℝ) = (↑(47 : ℕ) : ℝ) := by norm_cast
  rw [h47, ← Real.rpow_natCast]
  ring

/-- Full irrationality: `phi^47/4` is never a natural number. -/
theorem phi47_div_four_ne_nat (N : ℕ) :
    phi ^ (47 : ℕ) / 4 ≠ (N : ℝ) := by
  intro heq
  have h4 : (4 : ℝ) ≠ 0 := by norm_num
  have hpow : phi ^ (47 : ℕ) = (4 : ℝ) * N := by
    field_simp [h4] at heq
    linarith
  have hcast : (4 : ℝ) * N = ((4 * N : ℕ) : ℝ) := by
    push_cast; ring
  rw [hcast] at hpow
  exact phi_pow_ne_nat 47 (by norm_num) (4 * N) hpow

/-- **Export guard, with the reason proved.** `doubledEnergy_not_channelBlock-
Energy` rejects a doubled *event-energy kinematics* on the PairKernel pricing
layer, that is, a factor of two in energy. Doubling the T10 posted amplitude
does not double the window energy; it quadruples it, because window energy is
quadratic in the amplitude. The two decoys therefore differ by their factor
alone, before one even asks whether a bridge connects the layers, and no such
bridge is derived. Citing the pricing decoy as a T10 decoy rejection is wrong. -/
theorem doubledAmplitude_windowEnergy_eq_four_mul
    {a : ℝ} {ψ : LightPattern (Fin 8)}
    (hwin : SettledAnchorWindow a ψ) :
    normSq8 ((scalePattern 2 ψ).window 0) = 4 * normSq8 (ψ.window 0) := by
  have hnorm : normSq8 (ψ.window 0) = 2 * a ^ 2 := by
    rw [← neutralize_of_neutral (ψ.window 0) (settledAnchor_neutral hwin)]
    exact settledAnchor_neutralizedNormSq hwin
  have hwin2 : SettledAnchorWindow (2 * a) (scalePattern 2 ψ) :=
    scalePattern_settledAnchor 2 hwin
  have hnorm2 :
      normSq8 ((scalePattern 2 ψ).window 0) = 2 * (2 * a) ^ 2 := by
    rw [← neutralize_of_neutral ((scalePattern 2 ψ).window 0)
      (settledAnchor_neutral hwin2)]
    exact settledAnchor_neutralizedNormSq hwin2
  rw [hnorm, hnorm2]
  ring