IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CertifiedAnalyticTransformers
Countable registry of real values closed under rational constants and under unary/binary analytic protocol transformers. Supplies the inductive expression language and evaluation map used when certifying that native delta quantities stay inside a protocol-backed set. Downstream delta-native analysis and strong-closure modules import it as the ambient value universe. Structure is definitional: inductive expressions, recursive evaluation, and a closure theorem that every value carries a protocol.
claimA rich registry $\mathcal{R}$ is a countable set of reals generated from rational constants by unary and binary certified analytic protocol transformers. Each expression $e$ evaluates to a real $\mathrm{val}(e)\in\mathcal{R}$, the image is countable, and every value admits a protocol witness. The set is closed under $q\mapsto q$, addition, negation, and subtraction.
background
Primitive Recognition Calculus builds analytic certificates for quantities that appear in the Recognition forcing chain (J-cost, defects, phi-ladder gaps). The sibling module CertifiedAnalyticProtocols supplies the protocol layer: named analytic maps with certified real semantics. This module thickens that layer into a registry.
A rich expression is built from rational literals by applying unary or binary protocol transformers. Evaluation is the obvious recursive map into $\mathbb{R}$. The value set is the image of evaluation; countability follows because the expression grammar is countable. The design goal is a single ambient set large enough for native delta constructions yet small enough that every element still carries an explicit protocol certificate.
Local setting is Foundation-level scaffolding inside PrimitiveRecognitionCalculus: no physical constants are fixed here, only the analytic carrier used by later delta-native arguments.
proof idea
Definition module with a thin theorem layer. Inductive type for rich expressions; recursive evaluation into reals; value set as the image. Countability is by countable syntax. Pointwise lemmas record that rationals and the ring operations $+, -, \mathrm{neg}$ land in the value set when the corresponding transformers are in the registry. The main closure result states every value has an associated protocol, by induction on expression structure, discharging each constructor via the protocol data already attached to constants and transformers.
why it matters in Recognition Science
Delta-native analysis and delta-native strong closure both import this module as their value universe. Those downstream developments need a countable, protocol-certified carrier so that native delta quantities can be manipulated without leaving the certified-analytic fragment. Without the rich registry, protocol closure would stop at bare protocols and could not absorb the arithmetic combinations that appear when comparing defects, J-costs, or ladder increments. In the broader Recognition stack this is infrastructure beneath the forcing chain rather than a T0–T8 step itself: it keeps analytic certificates composable while later modules specialize to concrete delta identities.
scope and limits
- Does not define the protocol predicates themselves; those live in CertifiedAnalyticProtocols.
- Does not prove any physical identity about J, phi, mass rungs, or alpha.
- Does not assert completeness of the transformer list beyond the constructors present.
- Does not address continuity, differentiability rates, or numeric error bounds.
- Does not discharge delta-native strong closure; it only supplies the carrier.
used by (2)
depends on (1)
declarations in this module (16)
-
structure
RichRegistry -
inductive
RichExpr -
def
eval -
def
value -
def
values -
theorem
values_countable -
theorem
every_value_has_protocol -
theorem
value_rat -
theorem
value_add -
theorem
value_neg -
theorem
value_sub -
theorem
rich_transformer_closure -
def
composeUnary -
theorem
composeUnary_assoc -
def
composedUnary -
theorem
certified_transformer_headline