Foundation Dalembert Degree Exclusion Quadrupling Ring

The quadrupling identity

The declaration quadrupling_ring is a small but load-bearing algebraic identity. It states that if a function G satisfies a particular cubic composition law, then the value of G at four times an input can be expressed as a specific polynomial in the value of G at the input itself. The identity is a polynomial equation: it relates G(4s) to G(s) through a formula involving powers of G(s). This is not a statement about the physical world; it is a fact about how the composition law forces the function to behave at multiples of its argument.

The identity is proved by a machine-checked library of formal theorems. The proof is a direct algebraic expansion, a calculation that verifies the two sides of the equation are identical. This is the kind of step that a human mathematician would call routine, but the machine checks every symbol. The declaration is one of several similar identities, each for a different multiple: doubling, tripling, and quadrupling. Together, they provide the raw material for a larger argument.

The larger argument is the exclusion of degree-three polynomial combiners. The question is whether a continuous, nonconstant function can satisfy a composition law of the form G(t+u) + G(t-u) = 2G(t) + 2G(u) + G(t)²G(u) + G(t)G(u)². The quadrupling identity, along with its doubling and tripling counterparts, feeds into a contradiction. The contradiction arises because the two sides of a required identity have different polynomial degrees: one side has degree 9, the other degree 15. The mismatch forces the function to be zero everywhere, contradicting nonconstancy.

In Recognition Science, this exclusion is significant. It closes a gap in the d'Alembert Inevitability Theorem, showing that the degree-two assumption on the combiner is not an extra hypothesis but a forced consequence. The framework models recognition events as a ledger, a discrete record, and the cost of recognition is forced by the structure of the ledger. The exclusion of degree-three combiners is a step in showing that only the quadratic cost function is possible. The declaration itself, however, does not prove the exclusion; it only provides one of the algebraic pieces.

The declaration does not claim anything about the physical world. It does not state that recognition events occur, that a ledger exists, or that the cost function is unique. It is a purely mathematical statement about a function satisfying a given equation. The identity is true for any function that satisfies the composition law, regardless of whether that function has any physical meaning. The significance for Recognition Science is an interpretation placed on the result, not a consequence of the identity itself.

/-- **Ring identity (G(4s))**: Expanding `P(G(2s), G(2s))`. -/
lemma quadrupling_ring (a : ℝ) :
    2 * (4 * a + 2 * a ^ 3) + 2 * (4 * a + 2 * a ^ 3) +
    (4 * a + 2 * a ^ 3) ^ 2 * (4 * a + 2 * a ^ 3) +
    (4 * a + 2 * a ^ 3) * (4 * a + 2 * a ^ 3) ^ 2 =
    16 * a + 136 * a ^ 3 + 192 * a ^ 5 + 96 * a ^ 7 + 16 * a ^ 9 := by ring

/-- **Ring identity (G(4s))**: Expanding `P(G(2s), G(2s))`. -/
lemma quadrupling_ring (a : ℝ) :
    2 * (4 * a + 2 * a ^ 3) + 2 * (4 * a + 2 * a ^ 3) +
    (4 * a + 2 * a ^ 3) ^ 2 * (4 * a + 2 * a ^ 3) +
    (4 * a + 2 * a ^ 3) * (4 * a + 2 * a ^ 3) ^ 2 =
    16 * a + 136 * a ^ 3 + 192 * a ^ 5 + 96 * a ^ 7 + 16 * a ^ 9 := by ring

/-- **Degree-3 Exclusion Theorem.**

No function `G : ℝ → ℝ` satisfying the degree-3 polynomial composition law
  `G(t+u) + G(t-u) = 2G(t) + 2G(u) + G(t)²G(u) + G(t)G(u)²`
with `G(0) = 0` can be nonconstant. Every such function is identically zero.

The combiner `P(s,r) = 2s + 2r + s²r + sr²` is the minimal symmetric
degree-3 polynomial satisfying `P(0,v) = 2v` (with the `cuv` coefficient set to 0).
The proof works for any value of this coefficient. -/
theorem no_degree3_composition (G : ℝ → ℝ)
    (hFE : ∀ t u : ℝ, G (t + u) + G (t - u) =
      2 * G t + 2 * G u + G t ^ 2 * G u + G t * G u ^ 2)
    (hG0 : G 0 = 0) :
    ∀ s : ℝ, G s = 0 := by
  intro s
  -- Step 1: G(2s) = 4a + 2a³ from the functional equation at (s, s)
  have h1 := hFE s s
  rw [sub_self, hG0, add_zero] at h1
  have hG2 : G (s + s) = 4 * G s + 2 * (G s) ^ 3 := by
    linarith [doubling_ring (G s)]
  -- Step 2: G(3s) = 9a + 24a³ + 18a⁵ + 4a⁷ from FE at (2s, s)
  have h2 := hFE (s + s) s
  rw [show (s + s : ℝ) - s = s from by ring, hG2] at h2
  have hG3 : G (s + s + s) =
      9 * G s + 24 * (G s) ^ 3 + 18 * (G s) ^ 5 + 4 * (G s) ^ 7 := by
    linarith [tripling_ring (G s)]
  -- Step 3: G(4s) = 16a + 136a³ + 192a⁵ + 96a⁷ + 16a⁹ from FE at (2s, 2s)
  have h3 := hFE (s + s) (s + s)
  rw [sub_self, hG0, add_zero, hG2] at h3
  have hG4 : G (s + s + (s + s)) =
      16 * G s + 136 * (G s) ^ 3 + 192 * (G s) ^ 5 +
      96 * (G s) ^ 7 + 16 * (G s) ^ 9 := by
    linarith [quadrupling_ring (G s)]
  -- Step 4: The key identity from FE at (3s, s)
  have h4 := hFE (s + s + s) s
  rw [show (s + s + s : ℝ) + s = s + s + (s + s) from by ring,
      show (s + s + s : ℝ) - s = s + s from by ring,
      hG4, hG2, hG3] at h4
  -- Step 5: Extract the polynomial mismatch
  have hmismatch : 300 * (G s) ^ 5 + 830 * (G s) ^ 7 + 924 * (G s) ^ 9 +
      516 * (G s) ^ 11 + 144 * (G s) ^ 13 + 16 * (G s) ^ 15 = 0 := by
    linarith [lhs_expansion (G s), rhs_expansion (G s)]
  -- Step 6: The mismatch polynomial vanishes only at 0
  exact mismatch_forces_zero (G s) hmismatch

What this page does not claim

The declaration does not prove that the cost function is unique. The declaration does not state that recognition events occur in the physical world. The declaration does not establish the existence of a ledger.

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/DAlembert/DegreeExclusion.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: