enters
plain-language theorem explainer
Audit script certifying that the cost-unit stack (J-cost uniqueness, gauge-orbit classification, unit-from-minimality) depends only on Lean’s three ambient axioms, with the six-exponentials input carried as a named hypothesis rather than smuggled in as an axiom. Anyone citing T5 J-uniqueness or the law-of-logic cost theorem would run this check. There is no proof body: the certificate is a battery of `#print axioms` commands.
Claim. Every listed cost-unit declaration reports axiom footprint $\{ \mathrm{propext},\, \mathrm{Classical.choice},\, \mathrm{Quot.sound} \}$ only. The six-exponentials input, when present, appears as an explicit hypothesis in the type and is therefore invisible to the axiom printer. Nondegeneracy dichotomy results (vanishing at two, positive charge at two, sign-gauge orientation) take no six-exponentials hypothesis at all.
background
Recognition Science forces the J-cost $J(x)=(x+x^{-1})/2-1$ as the unique reciprocal continuous solution of the Recognition Composition Law (RCL), with normalization and calibration (T5 in the forcing chain). Downstream cost modules classify gauge orbits of multiplicative powers, extract the cost unit from minimality over powers, and tripwire against a defective full-filter reading of log curvature.
The ambient Lean kernel admits exactly three axioms: propositional extensionality, classical choice, and quotient soundness. Any further mathematical assumption must sit in the type as a named hypothesis; otherwise #print axioms would surface it. Upstream, law_of_logic_forces_jcost states uniqueness of $J$ under reciprocity, normalization, RCL, and calibration (using an internal Aczél smoothness package). The tripwire hasLogCurvature_full_filter_forces_zero forces curvature constant $\kappa=0$, so the calibrated value $\kappa=1$ is satisfied by no function.
This script lives outside the library proper: it imports the gauge-orbit, unit-from-minimality, monotone-power, and functional-equation modules and re-checks their axiom footprints in one place.
proof idea
No tactic or term proof. The module is a pure audit: successive #print axioms calls on the cost-unit stack. Targets include the six-exponentials-gated gauge-orbit family, monotone-power exponent existence, the full nondegeneracy dichotomy (vanishes-at-two characterizations, positive charge at two, strict-somewhere equivalence, sign-gauge orientation), unit-from-minimality comparisons, law_of_logic_forces_jcost, and the log-curvature tripwire. Pass criterion: each report lists only the three ambient axioms. Named hypotheses never appear in that report by construction of the printer.
why it matters
Without a clean axiom audit, T5 J-uniqueness and the unit-from-minimality anchor could silently depend on extra classical or analytic axioms, undermining the claim that the ledger alone decides nondegeneracy. Downstream consumers include residual bounds for $\alpha^{-1}$ in the CODATA band, uniqueness of $\lambda_{\mathrm{rec}}$, baryogenesis staging (orientation-odd sphaleron and Yukawa constraints, $\nu_R$ susceptibility split), $g_\star$ bookkeeping, and $\Omega_\Lambda$ tick-addressing. The script’s nondegeneracy block is the operational claim that the degenerate-versus-charging split is internal to the cost kernel, not an external analytic hypothesis. Framework landmarks touched: T5 J-uniqueness, RCL, and the calibrated cost that feeds constants ($\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, $\alpha^{-1}$ band).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.