IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CertifiedAnalyticTransformers
Defines a richer countable registry of real values closed under rational constants and under unary and binary analytic protocol transformers. Recognition analysts cite it when they need every generated value to carry a certified analytic protocol. The module is definitional: it builds an expression language, an evaluation map, and proves countability plus protocol inheritance by structural induction.
claimA countable registry $\mathcal{R}$ of real numbers containing $\mathbb{Q}$ and closed under certified unary maps $f$ and binary maps $g$ drawn from analytic protocols: if $x,y\in\mathcal{R}$ then $f(x),g(x,y)\in\mathcal{R}$, and every value inherits a protocol certificate.
background
In the Primitive Recognition Calculus, analytic identities used downstream (native $\Delta$ estimates, strong closure) must be tracked by certificates rather than bare reals. The upstream module CertifiedAnalyticProtocols supplies the protocol layer: each allowed transformer is a named analytic operation with a formal certificate.
This module thickens that layer into a free expression algebra. RichExpr is the inductive syntax (rationals, unary applications, binary applications). RichRegistry is the set of denotations under eval. The value family packages a real together with a witness that it arises from some expression, so protocol data can be recovered by recursion on syntax.
The local setting is foundation-level bookkeeping: no physics constants are fixed here. The goal is a countable, protocol-closed carrier on which later $\Delta$-native analysis can quantify without leaving the certified fragment.
proof idea
This is primarily a definition module. RichExpr and eval are inductive; value is the image type. Countability of the value set is the standard argument that a countable signature generates a countable term model. Protocol inheritance (every_value_has_protocol) and the concrete closure lemmas (value_rat, value_add, value_neg, value_sub, rich_transformer_closure) proceed by induction on the expression, applying the corresponding protocol constructors from CertifiedAnalyticProtocols at each node.
why it matters in Recognition Science
DeltaNativeAnalysis and DeltaNativeStrongClosure import this module as their certified carrier. Without a countable protocol-closed registry, native $\Delta$ bounds would either quantify over bare reals (losing certificates) or over an ad hoc finite list (losing closure under the transformers those proofs need). The richer registry is the intermediate object that lets strong-closure arguments stay inside the certified analytic fragment while still using rationals and the standard field operations. It sits under the Primitive Recognition Calculus stack that eventually supports forcing-chain analytic steps, not under T5–T8 directly.
scope and limits
- Does not define the analytic protocols themselves; those live in CertifiedAnalyticProtocols.
- Does not prove any $\Delta$-native estimate or strong-closure theorem.
- Does not claim the registry equals all reals or all computable reals.
- Does not introduce Recognition constants ($\phi$, $J$, eight-tick data).
- Does not address convergence rates or numeric approximation error.
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