Pith. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.NoHiddenState

show as:
view Lean formalization →

The NoHiddenState module establishes that a no-hidden-state finite comparison yields a counted-once composition law for the cost function C. Researchers tracing the Recognition Science derivation of the Recognition Composition Law would cite this result. The module organises the argument through three sibling declarations that link the LinearLogicBridge syntax directly to the counted-once normal form.

claimUnder the no-hidden-state condition there exists a counted-once resource expression $E$ such that the composite cost $C$ is obtained by evaluating $E$ on the two constituent costs.

background

This module belongs to the LogicAsFunctionalEquation series in the Foundation layer. It imports LinearLogicBridge, whose doc-comment states that the module formalises the normal-form version of counted-once resource syntax in which each constituent comparison appears at most once and the only scalar monomials are 1, u, v, and u*v.

The central declaration asserts a no-hidden-state composition law for C: a counted-once resource expression whose evaluation on the two constituent costs recovers the composite cost. The module therefore supplies the middle link between scale-free comparison and the RCL family.

proof idea

This is a definition module, no proofs. Its structure is carried by the three sibling declarations NoHiddenStateComposition, no_hidden_state_implies_counted_once, and no_hidden_state_comparison_forces_rcl.

why it matters in Recognition Science

This module supplies the middle step in the MainTheorem package, whose doc-comment describes the formal chain closest to the paper's headline: scale-free comparison factors through positive ratios; no-hidden-state finite comparison gives counted-once composition; counted-once finite logical comparison forces the RCL family. It therefore advances the Recognition Science derivation from the LinearLogicBridge syntax to the Recognition Composition Law.

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)