Gravity Corrected Taylor Higher Cardinality

The corrected Taylor gate

In Recognition Science, a ledger, a discrete record of events, is tested by whether local rules on a small patch force the same structure at every scale. The corrected Taylor gate is one such test: it asks whether a corrected quadratic correspondence, a local relationship between neighboring points, holds on a periodic grid, a torus of side length N. The module CorrectedTaylorHigherCardinality proves that if this correspondence holds on a cubic torus of side N for every N, then it holds on any rectangular torus, and conversely.

The central theorem is an equivalence. The all-cardinality gate, the statement that the correspondence holds on every valid periodic torus, is equivalent to the conjunction of two things: the cubic gate at every scale N, and a reverse implication from cubic to all-cardinality. The forward direction is trivial: a cubic torus is a special case of a rectangular one. The reverse direction is the nontrivial analytic step, and it remains open. The module proves the equivalence as a theorem, not the reverse implication itself.

A second theorem establishes a necessary algebraic condition. Any functional that is exactly quadratically homogeneous, meaning Q(a·ξ) = a²·Q(ξ), must be even: Q(-ξ) = Q(ξ). This matters because the Regge action, a discrete gravity action, is even in the displacement, so the flat configuration is a critical point. The proof uses only the homogeneity hypothesis with a = -1, no finite certificate, so it holds at every cardinality.

The module also connects to the previously closed N = 5 case. If the N = 5 gate implies the local correspondence at N = 5, then the cubic gate at N = 5 follows. This uses the existing N = 5 certificate as a hypothesis in a parameterized framework, not as a standalone re-export. The all-cardinality generalization remains open; the module reduces it to a single uniform identity plus one implication.

In plain language, the module does not prove the corrected Taylor gate at all scales. It proves that the whole problem reduces to checking one uniform identity at every scale, and that a necessary algebraic condition holds everywhere. The reverse implication from cubic to all-cardinality is the remaining open step, and the module names it precisely.

/-- **EQUIVALENCE WITH REVERSE HYPOTHESIS.** The all-cardinality gate is
equivalent to the conjunction of (a) the cubic gate at every `N` and (b) the
reverse implication from cubic to all-cardinality. This reduces the
all-cardinality gate to a single uniform parameterized identity (the cubic
gate) plus one implication. -/
theorem allCardinalityGate_iff_cubic_and_reverse :
    AllCardinalityCorrectedGate ↔
    (∀ (N : ℕ) [NeZero N] (hN : 2 < N), CorrectedTrack1BGateAtCubic N hN) ∧
    CubicGateImpliesAllCardinality := by
  constructor
  · intro h
    refine ⟨fun N _ hN => h N N N hN hN hN, ?_⟩
    intro _
    exact h
  · rintro ⟨hcub, hrev⟩
    exact hrev hcub

/-- Any exactly quadratically homogeneous functional on a real vector space
is *even*: `Q(-ξ) = Q(ξ)`. This is a necessary algebraic condition for the
correspondence at any cardinality, since the Regge action is even in the
displacement (the flat configuration is a critical point). The proof uses
only the homogeneity hypothesis with `a = -1` and `norm_num` — no
`native_decide`, no finite certificate. -/
theorem homogeneous_quadratic_is_even
    {V : Type*} [AddCommGroup V] [Module ℝ V]
    (Q : V → ℝ)
    (hQ : ∀ (a : ℝ) (ξ : V), Q (a • ξ) = a ^ (2 : ℕ) * Q ξ)
    (ξ : V) :
    Q (-ξ) = Q ξ := by
  have h : (-1 : ℝ) • ξ = -ξ := by
    rw [neg_smul, one_smul]
  rw [← h, hQ]
  norm_num

/-- **FORWARD REDUCTION.** The all-cardinality corrected gate implies the
cubic gate at every scale `N ≥ 3`. This is the trivial direction: the cubic
case (`Nx = Ny = Nz = N`) is a special case of the general case. -/
theorem allCardinalityGate_implies_cubicGate
    (h : AllCardinalityCorrectedGate)
    (N : ℕ) [NeZero N] (hN : 2 < N) :
    CorrectedTrack1BGateAtCubic N hN :=
  h N N N hN hN hN

/-- **CONDITIONAL N=5.** If the `N = 5` gate (the finite coefficient identity,
already closed via `native_decide` in `FreudenthalAxisStencilCoeffCert`)
implies the local correspondence at `N = 5`, then the cubic gate at `N = 5`
follows. This uses the existing `N = 5` certificate in a new way — as a
hypothesis in a parameterized framework, not as a standalone re-export. -/
theorem correctedTrack1BGateAtCubic_five_of_gateImp
    (hImp : CanonicalPeriodicCorrectedTrack1BGateAtN5 →
      CorrectedTrack1BGateAtCubic 5 (by decide)) :
    CorrectedTrack1BGateAtCubic 5 (by decide) :=
  hImp correctedTrack1BGateAtN5_closed

What this page does not claim

The all-cardinality corrected gate is not proved; only its equivalence to a cubic gate plus a reverse implication is proved. The reverse implication from cubic to all-cardinality is not proved; it remains open. The N = 5 certificate is not re-exported here; it is used as a hypothesis in a conditional theorem.

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/Gravity/CorrectedTaylorHigherCardinality.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: