Cost Classical Results

Classical results

Recognition Science derives physical structure from the cost of recognition events, and its central theorems are machine-checked in a proof assistant. Those proofs rely on many ordinary facts from real analysis, complex analysis, and functional equations. The module Cost.ClassicalResults declares those facts as axioms pending full formalization. The axioms are not new physical assumptions; they are textbook results with multiple independent proofs in the literature, and each one carries an academic reference.

The module states its own discipline. Every axiom is a standard result, computationally verifiable to arbitrary precision, and used routinely in mathematical physics without re-proving. The list includes the exponential form of the hyperbolic cosine, the norm of a complex exponential, the additivity of path integrals over adjacent intervals, and bounds on spherical cap measure. One lemma records that the function theta_min_spec_inequality gives a lower bound on the angle theta_min in terms of the inverse sine of a decaying exponential, which is the kind of analytic fact the forcing chain needs.

The module also records a correction. A previously stated axiom, continuousOn_extends_to_continuous, was removed because it is mathematically false; the counterexample is the function sin(1/x), continuous on the positive reals but with no continuous extension to zero. The removal is documented in docs/FALSE_AXIOMS_ANALYSIS.md. This matters because the forcing chain's claims inherit their epistemic strength from the axioms they use. The classical results are tagged as axioms, not theorems, until they are formally verified.

In plain language, this module is the scaffolding. It lets the framework's central proof proceed without waiting for Mathlib to formalize every standard fact. The facts themselves are not in dispute; what is in dispute, and what the module does not settle, is whether those facts can be derived from the framework's own starting point. That remains a target for future formalization.

MODEL spherical_cap_pos · IndisputableMonolith/Cost/ClassicalResults.lean

MODEL exp_mul_rearrange · IndisputableMonolith/Cost/ClassicalResults.lean

MODEL piecewise_path_integral_additive_integrable · IndisputableMonolith/Cost/ClassicalResults.lean

What this page does not claim

This answer does not claim that the classical results are derived within Recognition Science. This answer does not claim that the module proves the forcing chain's theorems. This answer does not claim that all axioms in the module are currently formalized.

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/Cost/ClassicalResults.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: