Foundation Pair Kernel Native Action Quantum Native Action Quantum Inv Pi Free

The pi-free certificate

The golden ratio φ, about 1.618, is the number that solves r² = r + 1. The Recognition Science framework derives this number as the unique self-similar scaling forced by its cost law, and then uses it to build physical constants. One of those constants is the native action quantum, the framework's smallest unit of action, which it writes as φ⁻⁵. The declaration nativeActionQuantumInv_piFree is a machine-checked certificate that this value, and its reciprocal φ⁵, can be expressed using only the golden ratio and arithmetic operations, with no dependence on pi.

The certificate works by building a ledger expression, a formal tree of multiplications and inverses starting from the golden ratio as an atom. The expression for φ⁵ is simply φ multiplied by itself five times. The expression for the action quantum is the inverse of that. The machine-checked library of formal theorems then evaluates these expressions and proves they equal the real numbers φ⁵ and φ⁻⁵. The key theorem, nativeActionQuantumInv_piFree, states that this reciprocal value is pi-free, meaning its construction never introduces the constant π. The proof is direct: the expression contains only the golden ratio atom, so the pi-free property follows by construction.

The certificate also records a structural fact about the framework's geometry. A recognition event, the basic unit of the framework's ledger, has a configuration dimension equal to the spatial dimension plus two: one degree for a temporal tick and one for the ledger balance. At the framework's forced spatial dimension of three, this count is five. The theorem nativeActionQuantum_exponent_eq_configDim connects these two ideas, showing that the exponent in the action quantum, φ⁻⁵, is exactly the configuration dimension of a recognition event at that spatial dimension. This is a bridge between the geometric counting of degrees of freedom and the algebraic expression for the action unit.

What this certificate does not do is select the numerical magnitude of the pair-kernel source. The docstring is explicit: this certificate does not by itself choose that magnitude. It also does not claim that the action quantum is the measured Planck constant; the framework's constants are derived in its own units, and the comparison to measured physics is a separate empirical check. The certificate is a statement about the internal grammar of the framework's expressions, not about experimental data.

theorem nativeActionQuantum_eq_inv_phi_pow_five :
    nativeActionQuantum = (goldenRatio ^ (5 : ℕ))⁻¹ := by
  unfold nativeActionQuantum nativeActionQuantumExpr LedgerExpr.eval
  rw [phiPow5Expr_eval]

theorem nativeActionQuantumInv_piFree : PiFree nativeActionQuantumInv :=
  piFree_eval nativeActionQuantumInvExpr

/-- Configuration-dimension bridge: the Nat exponent equals `configDim 3`. -/
theorem nativeActionQuantum_exponent_eq_configDim :
    nativeActionQuantum = (goldenRatio ^ configDim spatialDim)⁻¹ := by
  rw [nativeActionQuantum_eq_inv_phi_pow_five, configDim_at_spatial3]

What this page does not claim

This certificate does not select the pair-kernel source magnitude. This certificate does not prove the action quantum equals a measured physical constant. This certificate does not claim the framework's derivation of the spatial dimension is complete.

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/PairKernelNativeActionQuantum.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: