Foundation Pair Kernel Weyl Event Center Attachment Finite Fourier Exchange Inva

Equal weights under a Fourier exchange

In the Recognition Science framework, a recognition event is a discrete record of a comparison, and each such event carries a cost, a real number measuring how expensive that comparison is. The framework models certain recognition processes on a small finite carrier: a three-axis structure with 27 sites, which the framework identifies with a discrete torus. On each axis, a configuration is described by three complex amplitudes, one per site. Two basic costs appear: a shift cost, which penalizes differences between neighboring amplitudes, and a clock cost, which penalizes deviations from a fixed reference phase. A general cost combines them with two weights, one for shifts and one for clocks.

The theorem finiteFourierExchangeInvariant_forces_equal_weights proves a conditional statement. Suppose the two-weight cost is invariant under a discrete Fourier transform: applying the transform to any configuration multiplies the total cost by exactly 3, the size of the axis. That invariance is a strong symmetry, exchanging the roles of shift and clock costs. The theorem shows that, under that premise, the two weights must be equal. In plain terms: if the cost cannot tell a configuration apart from its Fourier-transformed version, then shifts and clocks must be priced the same. The proof is machine-checked; the declaration is a theorem in the framework's library, with no unproved assumptions beyond the stated premise.

The theorem does not claim that the premise actually holds. The framework's existing results do not yet supply a physical reason why the finite Fourier exchange invariance should be true. The docstring states this plainly: the equal-weight claim remains OPEN. The theorem is a conditional bridge, not an unconditional derivation. It also does not introduce any dimensioned length or any empirical constant; the statement is purely combinatorial and analytic, about a finite set of complex amplitudes.

What the theorem buys, if the premise is ever established, is a genuine simplification: the two independent weights collapse into one. Until then, the framework treats them as separate parameters. The declaration sits inside a larger module that attaches a clock center to a realized posting, but the equal-weight result is independent of that attachment; it is a fact about the axis-level cost alone.

/-- A genuine finite-Fourier exchange symmetry would force equal shift and
clock weights.  The conclusion is conditional on `hinvariant`. -/
theorem finiteFourierExchangeInvariant_forces_equal_weights
    {shiftWeight clockWeight : ℝ}
    (hinvariant :
      FiniteFourierExchangeInvariantAxis3
        shiftWeight clockWeight) :
    shiftWeight = clockWeight := by
  have h := hinvariant deltaAxisAmplitude3
  rw [finiteDFTAxis3_delta] at h
  simp only [twoWeightOccupationCostAxis3,
    shiftOccupationCostAxis3_uniform,
    clockOccupationCostAxis3_uniform,
    shiftOccupationCostAxis3_delta,
    clockOccupationCostAxis3_delta,
    mul_zero, add_zero] at h
  linarith

What this page does not claim

The finite Fourier exchange invariance is not proved to hold in the framework. The theorem does not derive any empirical constant or dimensioned length. The theorem does not establish that the two-weight cost is the unique or preferred cost for the carrier.

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/Foundation/PairKernelWeylEventCenterAttachment.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: