Post-collapse bracket interface for R-324

This module isolates the smallest bracket-retaining analytic input on the actual residual-refined physical carrier. The input is deliberately unweighted: r324RefinedPhysicalIntegral is exactly the unweighted finite contraction sum momentRefinedDeterministicTermSum. The factor |lamEps lam ε|^(2*m) is introduced only later, when the refined fibres are reassembled into deterministicMomentPairingSum.

It also records the direct reduction from the arbitrary-finite-set capped bracket ledger to the refined-fibre Hdet ledger, without adding the unrelated phase-free density clause of R324CappedCrossLedgerStrong.

def Anderson4D.R324RefinedPostCollapseBracketBound (ρ : SmoothCutoff) (K : ℝ) : Prop

The post-collapse bracket bound on one realized refined schedule.

The norm is outside the complete signed physical integral of the refined fibre. In particular, no norm is taken inside a covariance-key sum. The statement carries no lamEps factor because its exact downstream target, R324HdetBracketLedgerBound, bounds the unweighted deterministic fibre sum.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324RefinedPostCollapseBracketBound.toHdetBracketLedger {ρ : SmoothCutoff} {K : ℝ} (h : R324RefinedPostCollapseBracketBound ρ K) : R324HdetBracketLedgerBound ρ K

The physical refined-schedule bound is exactly the Hdet bracket ledger. The bridge is an equality of the two unweighted signed fibre expressions, so no coupling or logarithmic normalization is introduced here.

theorem Anderson4D.R324CappedBracketDensityLedger.toHdetBracketLedger {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : R324CappedBracketDensityLedger ρ K) : R324HdetBracketLedgerBound ρ K

The capped arbitrary-finite-set bracket ledger implies the Hdet refined-fibre ledger directly. This is the bracket half of R324CappedCrossLedgerStrong.toBracket, with no phase-free density hypothesis.