pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.NoHiddenState

show as:
view Lean formalization →

The module establishes a no-hidden-state composition law for the cost function C. Finite comparisons without hidden states yield a counted-once resource expression whose evaluation on the constituent costs produces the composite cost. Researchers deriving the recognition composition law from logical comparisons cite this result. The argument applies the normal-form resource syntax from the linear logic bridge to perform the necessary reductions.

claimUnder the no-hidden-state condition there exists a counted-once resource expression $E$ such that the composite cost satisfies $C = E(C_1, C_2)$.

background

The module belongs to the LogicAsFunctionalEquation package in Recognition Science, which recasts logic as a functional equation for cost comparisons. It imports the linear logic bridge module, whose resource-sensitive syntax restricts comparisons to normal form with scalar monomials limited to 1, u, v, and u times v.

proof idea

The module opens with a definition of the no-hidden-state composition law. It then proves that this condition implies the existence of a counted-once resource expression for the composite cost. A second theorem shows that the resulting comparisons force the recognition composition law family. All steps reduce via the monomial restrictions supplied by the linear logic bridge.

why it matters in Recognition Science

This module supplies the intermediate result in the main theorem package for logic as functional equation. It establishes that no-hidden-state finite comparison produces counted-once composition, which connects the scale-free ratio step to the forcing of the recognition composition law family. The package collects this as the central bridge toward the paper's headline claim.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)