Gravity Corrected Taylor Higher Cardinality Corrected Track1 Bgate At Cubic

The cubic gate

The declaration CorrectedTrack1BGateAtCubic defines a precise mathematical statement about a discrete grid, not a physical law. A cube made of N×N×N points, arranged periodically so opposite faces wrap around. The statement asserts that a certain local relationship, called the corrected correspondence, holds at every interior point of this cube. This relationship compares two ways of computing a quantity from neighboring points: one from a simple stencil, the other from a Taylor expansion. The declaration says these two computations agree.

The theorem's power is in its reduction. The framework's ultimate goal, the all-cardinality gate, would assert this correspondence holds for every possible grid size and shape. That remains open. What the theorem proves is that this vast goal is equivalent to a simpler one: checking the correspondence on cubic grids of every side length N, plus one additional implication. This is a genuine step forward, turning an infinite family of checks into a single parameterized identity.

The proof also establishes a necessary algebraic property. Any functional that is exactly quadratic in its input, meaning it scales by the square of the scaling factor, must be even: flipping the sign of the input leaves the output unchanged. This is proved for all real vector spaces, with no reliance on finite computation. It applies directly to the axis stencil used in the correspondence, confirming that the flat configuration is a critical point, a natural requirement for a physical action.

Finally, the theorem makes a conditional connection at N=5. If the already-verified finite coefficient identity at N=5 implies the local correspondence, then the cubic gate at N=5 follows. This is a bridge from a known computational result to a statement in the parameterized framework, but the bridge itself is conditional. The implication is not yet proved.

What the declaration does not claim is equally important. It does not prove the all-cardinality gate, nor does it prove the cubic gate for any specific N, including N=5. The conditional N=5 result depends on an unproven implication. The theorem is a structural reduction and an algebraic necessary condition, not a proof of the correspondence itself.

/-- The corrected Track 1.B gate at cubic scale `N`: the local cubic-Taylor
correspondence with the axis stencil holds on the cubic Freudenthal torus
with side length `N`. For each `N`, this reduces to a finite coefficient
identity over the `N³` vertex table. -/
def CorrectedTrack1BGateAtCubic (N : ℕ) [NeZero N] (hN : 2 < N) : Prop :=
  CanonicalPeriodicAxisStencilLocalCorrespondence N N N hN hN hN

/-- **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

/-- **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 gate is not proved. The cubic gate is not proved for any specific N, including N=5. The theorem does not establish that the corrected correspondence holds on any actual grid. The N=5 connection is conditional on an unproven implication.

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: