IndisputableMonolith.Certificates.JMonotone
This module packages certificates for verifying monotonicity of the J-budget function within each window of an LNAL parse. LNAL invariant generators cite it when assembling preservation and bound checks. It is a definition-only module that introduces a certificate type and error constructor as a thin packaging layer.
claimCertificate package for per-window monotonicity diagnostics of the J-budget function in the LNAL parser.
background
The module sits in the Certificates domain and imports the LNAL parser together with the JBudget module. Its documentation states that it supplies a certificate package for per-window J-budget monotonicity diagnostics. The imported modules supply the window structures and the underlying J-cost function used in the diagnostics.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module feeds the LNAL invariants certificate in URCGenerators.LNALCerts, which bundles VM preservation and token δ-unit bound. It supplies the J-budget monotonicity diagnostics required to complete that certificate package.
scope and limits
- Does not prove the underlying J-monotonicity property.
- Does not handle interactions across multiple windows.
- Does not connect to the forcing chain steps T0-T8.