Gravity Corrected Taylor Higher Cardinality All Cardinality Gate Implies Cubic G

A reduction in scope

In the Recognition Science framework, a ledger (a discrete record of events) can be laid out on a periodic grid, and the framework studies whether a local rule, called the corrected Taylor gate, holds on that grid. The broadest possible claim is the all-cardinality gate: the rule holds on every valid periodic grid, whatever its side lengths in the three directions. The declaration allCardinalityGate_implies_cubicGate proves a logical reduction: if that broad claim is true, then the rule holds on every cube-shaped grid, where all three side lengths are equal.

The proof is one line. The cubic case is a special case of the general one, so assuming the general case gives the cubic case immediately. The declaration makes this explicit in the framework's machine-checked library of formal theorems. It also proves the converse direction as a separate statement: the all-cardinality gate is equivalent to the conjunction of the cubic gate at every scale plus a reverse implication, which would say that the cubic case forces the general one. That reverse implication is not proved; it remains a target.

What the declaration does not claim is just as important. It does not prove that the corrected Taylor gate actually holds on any grid. It only proves a conditional: if the all-cardinality gate holds, then the cubic gate holds. The all-cardinality gate itself, and the cubic gate at any fixed scale, remain open. The declaration also does not prove the reverse implication from cubic to all-cardinality; that is a nontrivial analytic step, stated as a proposition but not established.

In Recognition Science, this reduction matters because it narrows what must be checked. Instead of verifying the rule on every possible grid, one could in principle verify it on cube-shaped grids and then prove the reverse implication. The framework's library shows the logical shape of that task: the all-cardinality gate splits cleanly into a uniform cubic identity plus one additional implication. The reduction is a step toward making the larger claim tractable, not a proof of it.

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

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

What this page does not claim

The corrected Taylor gate holds on any grid. The cubic gate holds at any fixed scale. The reverse implication from cubic to all-cardinality is proved.

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: