Transport Licensing and Scope Overreach

Abstract

Licensed reports retain transport conditions and expansion reopens completion.

Theorem 1.1 (Unlicensed scope expansion is overreach).

$$\begin{array}{c}\mathrm{LicensedReport}\left(q,J,J^{\prime }\right)⟺\mathrm{reportedScope}\left(q\right)=J^{\prime }\wedge \exists \kappa ,\mathrm{ValidTransportCert}\left(\kappa ,r,\mathrm{concept}\left(q\right),J,J^{\prime },\mathrm{Version}\left(\mathrm{concept}\left(q\right)\right)\right)\wedge \mathrm{condition}\left(q\right)⟺\mathrm{GivenPremises}\left(\kappa \right)\wedge \mathrm{Holds}\left(\mathrm{TransportAssumption}\left(\kappa \right)\right)\wedge \\ \mathrm{LicensedReport}\left(q,J,J^{\prime }\right)\Rightarrow \mathrm{condition}\left(q\right)\Rightarrow \exists \kappa ,\mathrm{ValidTransportCert}\left(\kappa ,r,\mathrm{concept}\left(q\right),J,J^{\prime },\mathrm{Version}\left(\mathrm{concept}\left(q\right)\right)\right)\wedge \mathrm{GivenPremises}\left(\kappa \right)\wedge \mathrm{Holds}\left(\mathrm{TransportAssumption}\left(\kappa \right)\right)\wedge \\ \mathrm{LicensedReport}\left(q,J,J^{\prime }\right)\Rightarrow \exists \kappa ,\mathrm{ValidTransportCert}\left(\kappa ,r,\mathrm{concept}\left(q\right),J,J^{\prime },\mathrm{Version}\left(\mathrm{concept}\left(q\right)\right)\right)\wedge \mathrm{condition}\left(q\right)⟺\mathrm{GivenPremises}\left(\kappa \right)\wedge \mathrm{Holds}\left(\mathrm{TransportAssumption}\left(\kappa \right)\right)\wedge ((\neg \mathrm{GivenPremises}\left(\kappa \right)\vee \neg \mathrm{Holds}\left(\mathrm{TransportAssumption}\left(\kappa \right)\right))\Rightarrow \neg \mathrm{condition}\left(q\right))\wedge \\ \mathrm{Overreach}\left(q,J,J^{\prime }\right)⟺J\subset J^{\prime }\wedge J\ne J^{\prime }\wedge \mathrm{Scope}\left(\mathrm{concept}\left(q\right)\right)=J\wedge \mathrm{reportedScope}\left(q\right)=J^{\prime }\wedge \neg \mathrm{LicensedReport}\left(q,J,J^{\prime }\right)\wedge \\ \exists J_0,J_1,S,T,J_0\subset J_1\wedge J_0\ne J_1\wedge \mathrm{defectRelation}\left(\mathrm{restrict}\left(S,J_0\right),\mathrm{restrict}\left(T,J_0\right)\right)=\varnothing \wedge \mathrm{defectRelation}\left(\mathrm{restrict}\left(S,J_1\right),\mathrm{restrict}\left(T,J_1\right)\right)\ne \varnothing \wedge \\ \forall \kappa ,\mathrm{reportedScope}\left(q\right)=J^{\prime }\Rightarrow \mathrm{ValidTransportCert}\left(\kappa ,r,\mathrm{concept}\left(q\right),J,J^{\prime },\mathrm{Version}\left(\mathrm{concept}\left(q\right)\right)\right)\Rightarrow \mathrm{GivenPremises}\left(\kappa \right)\Rightarrow \mathrm{Holds}\left(\mathrm{TransportAssumption}\left(\kappa \right)\right)\Rightarrow \mathrm{LicensedReport}\left(q[\mathrm{condition}:=\mathrm{True}],J,J^{\prime }\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Transport/OverreachWithoutLicense.overreach_without_license (✓ std3). ∎

Source. Repository-derived.

Commentary.

A transport report q stores concept(q), its claimed operation scope J’, and its retained proposition condition(q). LicensedReport also checks that the stored scope equals the explicit J’, so the target domain cannot drift through a free argument.

ValidTransportCert is the concrete predicate imported from the transport-certificate validity module. Its arguments bind the certificate to the source record r, concept(q), old and claimed scopes, and Version(concept(q)); this module introduces no second validity definition.

A license retains condition(q) exactly as GivenPremises(kappa) conjoined with the certificate’s explicit transport-assumption obligations. Therefore an unconditional licensed report exposes proofs of both conjuncts, while a missing conjunct prevents the condition from being discharged.

Overreach is the conjunction of strict scope expansion, Scope(concept(q))=J, the report’s claim of J’, and absence of a license. No certificate validity or premise is inferred from the scope equations.

Section 35 informally assumes that the record space carries a distance, but it does not declare the comparison and supremum operations on abstract Delta, or the laws for those operations, that Lean needs for the later <= epsilon and above-epsilon notation. The tolerance clause is therefore not a conjunct of this theorem. A checked Boolean false neighbor records only that old-scope tolerance can fail after strict expansion. This paragraph and the matching module comment are human-readable only: they register neither digestion coverage nor an unresolved subitem. Ingest currently has no path for a newly discovered unresolved subitem; issue #3066 tracks that machine-registration gap.

CAS defines Closed_J(S,T) exactly by emptiness of defectRelation after restricting S and T to J. A concrete two-operation witness has an empty residual on its old singleton scope and a nonempty residual on the expanded scope, so expansion reopens local completion.

Conversely, when the report’s stored scope equals the claimed scope, a valid certificate together with every given premise and its transport assumption licenses the condition-update q[condition := True]. Without the premise and assumption proofs, the exact conditional statement remains the only licensed form.

Repository type-shape, English and Chinese synonym, and neighboring-module searches found no transport-license or overreach definition. Concept and the canonical defectRelation are reused; no second residual or closure predicate is introduced.

References

• Truth anchor: D5/S3/ConceptDynamics/Transport/OverreachWithoutLicense.overreach_without_license
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition
• Dependency: D5/S3/ConceptDynamics/TargetRisk/RefinementRiskCostTradeoff
• Dependency: D5/S3/ConceptDynamics/Transport/TransportCertificateValidity